. C. Bal03 and . Ballarin, Locales and locale expressions in isabelle/isar, TYPES, 2003.

C. B. Charron-bost, H. Debrat, and S. Merz, Formal Verification of Consensus Algorithms Tolerating Malicious Faults, Proceedings of SSS 2011, pp.120-134, 2011.
DOI : 10.1007/978-3-642-24550-3_11

URL : https://hal.archives-ouvertes.fr/hal-00639048

C. E. Clarke, Proving the correctness of coroutines without history variables, ACM-SE 16, pp.160-167, 1978.

C. M. Clint, Program proving: Coroutines, Acta Informatica, vol.6, issue.1, pp.50-63, 1973.
DOI : 10.1007/BF00571463

M. Clint, . T. Ct96, S. Chandra, and . Toueg, On the use of history variables, Proc. of ESOP, pp.15-30225, 1981.
DOI : 10.1007/BF00289587

M. J. Fischer, N. A. Lynch, and M. S. Paterson, Impossibility of distributed consensus with one faulty process, Journal of the ACM, vol.32, issue.2, pp.374-382, 1985.
DOI : 10.1145/3149.214121

F. R. Fuzzati, M. Merro, and U. , Distributed Consensus, revisited, Acta Informatica, vol.176, issue.1?2, pp.377-425, 2007.
DOI : 10.1007/s00236-007-0052-1

F. R. Fuzzati, A Formal Approach to Fault Tolerant Distributed Consensus, GL00. E. Gafni and L. Lamport. Disk Paxos Distributed Computing, pp.330-344, 2000.

G. Y. Gurevich, . M. Jm05, S. Jaskelioff, and . Merz, Evolving algebras: An attempt to discover semantics Proving the correctness of disk paxos. In The Archive of Formal Proofs, 1993.

L. L. Lamport, The implementation of reliable distributed multiprocess systems, Computer Networks (1976), vol.2, issue.2, pp.95-114, 1976.
DOI : 10.1016/0376-5075(78)90045-4

L. L. Lamport, The part-time parliament, ACM Transactions on Computer Systems, vol.16, issue.2, pp.133-169, 1998.
DOI : 10.1145/279227.279229

L. L. Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, 2002.

L. L. Lamport, R. Shostak, and M. Pease, The Byzantine Generals Problem, ACM Transactions on Programming Languages and Systems, vol.4, issue.3, pp.382-401, 1982.
DOI : 10.1145/357172.357176

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

L. N. Lynch, Distributed Algorithms, 1996.

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL -A Proof Assistant for Higher-Order Logic, LNCS, vol.2283, 2002.

. S. Owi76 and . Owicki, A consistent and complete deductive system for the verification of parallel programs, Proceedings of STOC '76 Sch90. F. B. Schneider. Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Computing Surveys, pp.73-86299, 1976.