A Constructive Proof of the Fischer-Lynch Paterson (FLP) Theorem in
the Logic of Events
 
The FLP result from 1985 states that consensus in an ansynchronous
distributed system in which one process can fail is impossible.  This
result is used by system developers to guide their designs, especially
in modern systems such as the Google File System.  The 1985 proof is
non-constructive as are all proofs since then that I know, even though
a hypothetical indecisive execution is the heart of the proof.  I show
how to recast the FLP result so that the construction of a waffling
computation can be carried out effectively, and I derive the original
result as a corollary of this fully constructive theorem which can be
proved in the Logic of Events formalized in computational type theory,
a constructive logical theory.  The result is a very simple new proof
of FLP and a reformulated stronger result that is even more useful in
practical program design.  I will discuss how these ideas are used in
our work to verify systems built around consensus protocols.