adam@310: @Book{TAPL,
adam@310:   author       = "Benjamin C. Pierce",
adam@310:   title        = "Types and Programming Languages",
adam@310:   year         = "2002",
adam@310:   publisher    = "MIT Press"
adam@310: }
adam@310: 
adam@310: @Book{CAR,
adam@310:   author       = "Matt Kaufmann and Panagiotis Manolios and J Strother Moore",
adam@310:   title        = "Computer-Aided Reasoning: An Approach",
adam@310:   year         = "2000",
adam@310:   publisher    = "Kluwer Academic Publishers"
adam@310: }
adam@310: 
adam@310: @Article{AMD,
adam@310:   author = {J Strother Moore and Tom Lynch and Matt Kaufmann},
adam@310:   title = {A Mechanically Checked Proof of the Correctness of the Kernel of the {AMD5k86} Floating-Point Division Algorithm},
adam@310:   journal = {IEEE Transactions on Computers},
adam@310:   volume = {47(9)},
adam@310:   pages = {913--926}
adam@310:   year = {1998}
adam@310: }
adam@310: 
adam@310: @Book{Piton,
adam@310:   author={J Strother Moore},
adam@310:   title = {Piton: A Mechanically Verified Assembly-Level Language},
adam@310:   year         = "1996",
adam@310:   series       = "Automated Reasoning Series",
adam@310:   publisher    = "Kluwer Academic Publishers"
adam@310: }
adam@310: 
adam@310: @Article{Nqthm,
adam@310:   title = {The {Boyer-Moore} Theorem Prover and Its Interactive Enhancement},
adam@310:   author = {Robert S. Boyer and Matt Kaufmann and J Strother Moore},
adam@310:   journal = {Computers and Mathematics with Applications},
adam@310:   volume = {29(2)},
adam@310:   year = {1995},
adam@310:   pages = {27--62}
adam@310: }
adam@310: 
adam@310: @Article{4C,
adam@310:   author = {Gonthier, Georges},
adam@310:   year = {2008},
adam@310:   title = {Formal Proof--The Four-Color Theorem},
adam@310:   journal = {Notices of the American Mathematical Society},
adam@310:   volume = {55(11)},
adam@310:   pages = {1382-–1393}
adam@310: }
adam@310: 
adam@310: @Article{CompCert,
adam@310:   author = {Leroy, Xavier},
adam@310:   year = {2009},
adam@310:   title = {A formally verified compiler back-end},
adam@310:   journal = {Journal of Automated Reasoning},
adam@310:   volume = {43(4)},
adam@310:   pages = {363--446}
adam@310: }
adam@310: 
adam@310: @InProceedings{seL4,
adam@310:     author =  {Gerwin Klein 
adam@310:     and Kevin Elphinstone 
adam@310:     and Gernot Heiser
adam@310:     and June Andronick 
adam@310:     and David Cock
adam@310:     and Philip Derrin
adam@310:     and Dhammika Elkaduwe
adam@310:     and Kai Engelhardt
adam@310:     and Rafal Kolanski
adam@310:     and Michael Norrish
adam@310:     and Thomas Sewell
adam@310:     and Harvey Tuch
adam@310:     and Simon Winwood},
adam@310:     title =        {{seL4}: Formal Verification of an {OS} Kernel},
adam@310:     booktitle =    {Proceedings of the 22nd {ACM Symposium on Operating Systems Principles}},
adam@310:     year =         {2009},
adam@310: }
adam@310: 
adam@310: @Book{Isabelle/HOL,
adam@310:   author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
adam@310:   title		= {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
adam@310:   publisher	= {Springer},
adam@310:   series	= {Lecture Notes in Computer Science},
adam@310:   volume	= 2283,
adam@310:   year		= 2002
adam@310: }
adam@310: 
adam@310: @Book{Isabelle,
adam@310:   author = {Paulson, Lawrence C.},
adam@310:   year = {1994},
adam@310:   title = {Isabelle: A Generic Theorem Prover},
adam@310:   series = {Lecture Notes in Computer Science},
adam@310:   volume = {828},
adam@310:   publisher = {Springer}
adam@310: }
adam@310: 
adam@310: @Book{CoqArt,
adam@310:   author       = "Bertot, Yves and Cast\'eran, Pierre",
adam@310:   title        = "Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions",
adam@310:   series       = "Texts in Theoretical Computer Science",
adam@310:   year         = "2004",
adam@310:   publisher    = "Springer Verlag",
adam@310: }
adam@310: 
adam@310: @unpublished{CoqManual,
adam@310:   author = "{Coq Development Team}",
adam@310:   title = "The {Coq} proof assistant reference manual, version 8.3",
adam@310:   year = 2010,
adam@310:   url={http://coq.inria.fr/refman/}
adam@310: }