A formal verification of the alternating bit protocol in the calculus of constructions / Marc Bezem, Jan Friso Groote
A formal verification of the alternating bit protocol in the calculus of constructions