[cap-talk] Static Typing for a Faulty Lambda Calculus

[Sandro Magi]

The dangers of random bit flips and the ensuing problems have been
mentioned and/or discussed on this list a few times over the years.
Here's a paper which defines:

"lambda-zap, a lambda calculus that exhibits intermittent data faults.
In order to detect and recover from these faults, lambda-zap programs
replicate intermediate computations and use majority voting, thereby
modeling software-based fault tolerance techniques studied extensively,
but informally. [...] This type system guarantees that well-typed
programs can tolerate any single data fault. To demonstrate that
lambda-zap can serve as an idealized typed intermediate language, we
define a type-preserving translation from a standard simply-typed lambda
calculus into lambda-zap."

http://lambda-the-ultimate.org/node/2108