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: }
adam@355: 
adam@355: @InBook{WinskelDomains,
adam@355:   author       = "Glynn Winskel",
adam@355:   title        = "The Formal Semantics of Programming Languages",
adam@355:   year         = "1993",
adam@355:   publisher    = "MIT Press",
adam@355:   chapter      = "8"
adam@355: }
adam@356: 
adam@356: @article{Capretta,
adam@356:   author     = {Venanzio Capretta},
adam@356:   title      = {General Recursion via Coinductive Types},
adam@356:   journal    = {Logical Methods in Computer Science},
adam@356:   volume     = 1,
adam@356:   number     = 2,
adam@356:   year       = 2005,
adam@356:   pages      = {1--18},
adam@356: }
adam@356: 
adam@356: @inproceedings{Megacz,
adam@356:  author = {Adam Megacz},
adam@356:  title = {A coinductive monad for prop-bounded recursion},
adam@356:  booktitle =   {Proceedings of the {ACM} Workshop Programming
adam@356:                 Languages meets Program Verification},
adam@356:  pages = {11--20},
adam@356:  year = {2007},
adam@356: }
adam@358: 
adam@358: @inproceedings{modules,
adam@358:  author = {MacQueen, David},
adam@358:  title = {Modules for {Standard ML}},
adam@358:  booktitle = {Proceedings of the 1984 ACM Symposium on LISP and Functional Programming},
adam@358:  year = {1984},
adam@358:  pages = {198--207},
adam@358: } 
adam@358: 
adam@358: @inproceedings{typeclasses,
adam@358:  author = {Wadler, P. and Blott, S.},
adam@358:  title = {How to make ad-hoc polymorphism less ad hoc},
adam@358:  booktitle = {Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
adam@358:  year = {1989},
adam@358:  pages = {60--76},
adam@358: }