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: } adam@311: adam@311: @inproceedings{CIC, adam@311: author = {Christine Paulin-Mohring}, adam@311: title = {Inductive Definitions in the System {Coq} - Rules and Properties}, adam@311: year = {1993}, adam@311: booktitle = {Proceedings of the International Conference on {Typed Lambda Calculi and Applications}}, adam@311: } adam@311: adam@311: @inproceedings{SetsInTypes, adam@311: author = {Benjamin Werner}, adam@311: title = {Sets in Types, Types in Sets}, adam@311: booktitle = {Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software}, adam@311: year = {1997}, adam@311: } adam@311: adam@311: @article{CoC, adam@311: author = {Thierry Coquand and G\'erard Huet}, adam@311: title = {The {Calculus} of {Constructions}}, adam@311: journal = {Information and Computation}, adam@311: volume = {76(2-3)}, adam@311: year = {1988} adam@311: } adam@312: adam@315: @inproceedings{GADT, adam@312: author = {Hongwei Xi and Chiyan Chen and Gang Chen}, adam@312: title = {Guarded Recursive Datatype Constructors}, adam@312: booktitle = {Proceedings of the 30th ACM SIGPLAN Symposium on Principles of Programming Languages}, adam@312: year = {2003} adam@312: } adam@315: adam@315: @article{Curry, adam@315: title={Functionality in Combinatory Logic}, adam@315: author = {H. B. Curry}, adam@315: journal = {Proceedings of the National Academy of Sciences of the United States of America}, adam@315: volume = {20(11)}, adam@315: year = {1934}, adam@315: pages = {584--590} adam@315: } adam@315: adam@315: @incollection{Howard, adam@315: author = {Howard, William A.}, adam@315: title = {The formulae-as-types notion of construction}, adam@315: editor = {Seldin, Jonathan P. and Hindley, J. Roger}, adam@315: booktitle = {To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism}, adam@315: publisher = {Academic Press}, adam@315: pages = {479--490}, adam@315: year = {1980}, adam@315: note = {Original paper manuscript from 1969} adam@315: }