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: } adam@316: adam@316: @inproceedings{HOAS, adam@316: author = {Pfenning, F. and Elliot, C.}, adam@316: title = {Higher-order abstract syntax}, adam@316: booktitle = {Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation}, adam@316: year = {1988}, adam@316: pages = {199--208}, adam@316: } adam@317: adam@317: @article{HOU, adam@317: author = {G\'erard Huet}, adam@317: title = {The undecidability of unification in third order logic}, adam@317: journal = {Information and Control}, adam@317: voluem = {22(3)}, adam@317: year = {1973}, adam@317: pages = {257--267} adam@317: } adam@328: adam@328: @InBook{TAPLNatDed, adam@328: author = "Benjamin C. Pierce", adam@328: title = "Types and Programming Languages", adam@328: year = "2002", adam@328: publisher = "MIT Press", adam@328: chapter = "9.4" adam@328: } adam@328: adam@328: @inproceedings{Monads, adam@328: author = {Wadler, Philip}, adam@328: title = {The essence of functional programming}, adam@328: booktitle = {Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, adam@328: year = {1992}, adam@328: } adam@328: adam@328: @inproceedings{IO, adam@328: author = {Peyton Jones, Simon L. and Wadler, Philip}, adam@328: title = {Imperative functional programming}, adam@328: booktitle = {Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, adam@328: year = {1993}, adam@328: } adam@328: adam@328: @InProceedings{separation, adam@328: author = {John C. Reynolds}, adam@328: title = {Separation Logic: A Logic for Shared Mutable Data Structures}, adam@328: booktitle = {Proceedings of the IEEE Symposium on Logic in Computer Science}, adam@328: year = {2002} adam@338: } adam@338: adam@338: @article{Okasaki, adam@338: author = {Okasaki, Chris}, adam@338: title = {Red-black trees in a functional setting}, adam@338: journal = {J. Funct. Program.}, adam@338: volume = {9}, adam@338: issue = {4}, adam@338: year = {1999}, adam@338: pages = {471--477}, adam@338: } adam@342: adam@342: @Article{DeBruijn, adam@342: author = "Nicolas G. de Bruijn", adam@342: title = "Lambda-calculus notation with nameless dummies: a tool for automatic formal manipulation with application to the {Church-Rosser} theorem", adam@342: journal = "Indag. Math.", adam@342: volume = "34(5)", adam@342: pages = "381--392", adam@342: year = "1972" adam@342: } adam@343: adam@343: @INPROCEEDINGS{GirardsParadox, adam@343: author = {Thierry Coquand}, adam@343: title = {An Analysis of {Girard's} Paradox}, adam@343: booktitle = {Proceedings of the Symposium on Logic in Computer Science}, adam@343: year = {1986}, adam@343: pages = {227--236} adam@343: } adam@344: adam@344: @inproceedings{PCC, adam@344: author = {George C. Necula}, adam@344: title = {Proof-carrying code}, adam@344: booktitle = {Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, adam@344: year = {1997}, adam@344: } adam@344: adam@344: @inproceedings{XCAP, adam@344: author = {Ni, Zhaozhong and Shao, Zhong}, adam@344: title = {Certified assembly programming with embedded code pointers}, adam@344: booktitle = {Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, adam@344: year = {2006}, adam@344: } adam@346: adam@346: @TechReport{IT, adam@346: title = "A Tutorial on Recursive Types in {Coq}", adam@346: author = "Eduardo Gim\'enez", adam@346: year = "1998", adam@346: month = may, adam@346: number = "0221", adam@346: institution = "INRIA", adam@346: } adam@347: adam@347: @inproceedings{BigStep, adam@347: author = {Xavier Leroy and Herv\'e Grall}, adam@347: title = {Coinductive big-step operational semantics}, adam@347: year = {2006}, adam@347: booktitle = {Proceedings of the 15th European Symposium on Programming} adam@347: }