@article{FLP,
 author = {Fischer, Michael J. and Lynch, Nancy A. and Paterson, Michael S.},
 title = {Impossibility of {D}istributed {C}onsensus with {O}ne {F}aulty {P}rocess},
 journal = {J. ACM},
 issue_date = {April 1985},
 volume = {32},
 number = {2},
 month = apr,
 year = {1985},
 issn = {0004-5411},
 pages = {374--382},
 numpages = {9},
 url = {http://doi.acm.org/10.1145/3149.214121},
 doi = {10.1145/3149.214121},
 acmid = {214121},
 publisher = {ACM},
 address = {New York, NY, USA},
} 

%@article{Voelzer,
 author = {Völzer, Hagen},
 title = {A {C}onstructive {P}roof for {FLP}},
 journal = {Inf. Process. Lett.},
 issue_date = {31 October 2004},
 volume = {92},
 number = {2},
 month = oct,
 year = {2004},
 issn = {0020-0190},
 pages = {83--87},
 numpages = {5},
 url = {https://doi.org/10.1016/j.ipl.2004.06.008},
 doi = {10.1016/j.ipl.2004.06.008},
 acmid = {1039319},
 publisher = {Elsevier North-Holland, Inc.},
 address = {Amsterdam, The Netherlands, The Netherlands},
 keywords = {concurrency, consensus problem, distributed computing, distributed systems, fault tolerance, formal modelling},
} 

@article{DBLP:journals/corr/cs-LO-9301106,
  author    = {Lawrence C. Paulson},
  title     = {Isabelle: {T}he {N}ext 700 {T}heorem {P}rovers},
  journal   = {CoRR},
  volume    = {cs.LO/9301106},
  year      = {1993},
  ee        = {http://arxiv.org/abs/cs.LO/9301106},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Kamm99,
 author = {Kamm\"{u}ller, Florian and Wenzel, Markus and Paulson, Lawrence C.},
 title = {Locales - A Sectioning Concept for Isabelle},
 booktitle = {Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics},
 series = {TPHOLs '99},
 year = {1999},
 isbn = {3-540-66463-7},
 pages = {149--166},
 numpages = {18},
 url = {http://dl.acm.org/citation.cfm?id=646526.694884},
 acmid = {694884},
 publisher = {Springer-Verlag},
 address = {London, UK, UK},
} 

@article{Buckley:1983:EIG:69624.357208,
 author = {Buckley, G. N. and Silberschatz, Abraham},
 title = {An {E}ffective {I}mplementation for the {G}eneralized {I}nput-{O}utput {C}onstruct of {CSP}},
 journal = {ACM Trans. Program. Lang. Syst.},
 issue_date = {April 1983},
 volume = {5},
 number = {2},
 month = apr,
 year = {1983},
 issn = {0164-0925},
 pages = {223--235},
 numpages = {13},
 url = {http://doi.acm.org/10.1145/69624.357208},
 doi = {10.1145/69624.357208},
 acmid = {357208},
 publisher = {ACM},
 address = {New York, NY, USA},
} 

@article{Kumar:1997:CAG:255377.255378,
 author = {Kumar, Devendra and Silberschatz, Abraham},
 title = {A {C}ounter-example to an {A}lgorithm for the {G}eneralized {I}nput-output {C}onstruct of {CSP}},
 journal = {Inf. Process. Lett.},
 issue_date = {March 28, 1997},
 volume = {61},
 number = {6},
 month = mar,
 year = {1997},
 issn = {0020-0190},
 pages = {287--},
 url = {https://doi.org/10.1016/S0020-0190(97)00040-9},
 doi = {10.1016/S0020-0190(97)00040-9},
 acmid = {255378},
 publisher = {Elsevier North-Holland, Inc.},
 address = {Amsterdam, The Netherlands, The Netherlands},
 keywords = {concurrency, distributed computing, program correctness, programming languages},
} 

@TechReport{Constable2011,
author = {Robert L. Constable},
title = {Effectively {N}onblocking {C}onsensus {P}rocedures {C}an {E}xecute {F}orever - a {C}onstructive {V}ersion of {FLP}},
institution = {Cornell University},
year = {2011},
OPTkey = {•},
OPTtype = {•},
number = {11513},
OPTaddress = {•},
OPTmonth = {•},
OPTnote = {•},
OPTannote = {•}
}