@Book{TAPL,
  author       = "Benjamin C. Pierce",
  title        = "Types and Programming Languages",
  year         = "2002",
  publisher    = "MIT Press"
}

@Book{CAR,
  author       = "Matt Kaufmann and Panagiotis Manolios and J Strother Moore",
  title        = "Computer-Aided Reasoning: An Approach",
  year         = "2000",
  publisher    = "Kluwer Academic Publishers"
}

@Article{AMD,
  author = {J Strother Moore and Tom Lynch and Matt Kaufmann},
  title = {A Mechanically Checked Proof of the Correctness of the Kernel of the {AMD5k86} Floating-Point Division Algorithm},
  journal = {IEEE Transactions on Computers},
  volume = {47(9)},
  pages = {913--926}
  year = {1998}
}

@Book{Piton,
  author={J Strother Moore},
  title = {Piton: A Mechanically Verified Assembly-Level Language},
  year         = "1996",
  series       = "Automated Reasoning Series",
  publisher    = "Kluwer Academic Publishers"
}

@Article{Nqthm,
  title = {The {Boyer-Moore} Theorem Prover and Its Interactive Enhancement},
  author = {Robert S. Boyer and Matt Kaufmann and J Strother Moore},
  journal = {Computers and Mathematics with Applications},
  volume = {29(2)},
  year = {1995},
  pages = {27--62}
}

@Article{4C,
  author = {Gonthier, Georges},
  year = {2008},
  title = {Formal Proof--The Four-Color Theorem},
  journal = {Notices of the American Mathematical Society},
  volume = {55(11)},
  pages = {1382-–1393}
}

@Article{CompCert,
  author = {Leroy, Xavier},
  year = {2009},
  title = {A formally verified compiler back-end},
  journal = {Journal of Automated Reasoning},
  volume = {43(4)},
  pages = {363--446}
}

@InProceedings{seL4,
    author =  {Gerwin Klein 
    and Kevin Elphinstone 
    and Gernot Heiser
    and June Andronick 
    and David Cock
    and Philip Derrin
    and Dhammika Elkaduwe
    and Kai Engelhardt
    and Rafal Kolanski
    and Michael Norrish
    and Thomas Sewell
    and Harvey Tuch
    and Simon Winwood},
    title =        {{seL4}: Formal Verification of an {OS} Kernel},
    booktitle =    {Proceedings of the 22nd {ACM Symposium on Operating Systems Principles}},
    year =         {2009},
}

@Book{Isabelle/HOL,
  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title		= {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  publisher	= {Springer},
  series	= {Lecture Notes in Computer Science},
  volume	= 2283,
  year		= 2002
}

@Book{Isabelle,
  author = {Paulson, Lawrence C.},
  year = {1994},
  title = {Isabelle: A Generic Theorem Prover},
  series = {Lecture Notes in Computer Science},
  volume = {828},
  publisher = {Springer}
}

@Book{CoqArt,
  author       = "Bertot, Yves and Cast\'eran, Pierre",
  title        = "Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions",
  series       = "Texts in Theoretical Computer Science",
  year         = "2004",
  publisher    = "Springer Verlag",
}

@unpublished{CoqManual,
  author = "{Coq Development Team}",
  title = "The {Coq} proof assistant reference manual, version 8.3",
  year = 2010,
  url={http://coq.inria.fr/refman/}
}

@inproceedings{CIC,
  author = {Christine Paulin-Mohring},
  title = {Inductive Definitions in the System {Coq} - Rules and Properties},
  year = {1993},
  booktitle = {Proceedings of the International Conference on {Typed Lambda Calculi and Applications}},
}

@inproceedings{SetsInTypes,
  author    = {Benjamin Werner},
  title     = {Sets in Types, Types in Sets},
  booktitle = {Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software},
  year      = {1997},
}

@article{CoC,
  author = {Thierry Coquand and G\'erard Huet},
  title = {The {Calculus} of {Constructions}},
  journal = {Information and Computation},
  volume = {76(2-3)},
  year = {1988}
}

@inproceedings{GADT,
  author = {Hongwei Xi and Chiyan Chen and Gang Chen},
  title = {Guarded Recursive Datatype Constructors},
  booktitle = {Proceedings of the 30th ACM SIGPLAN Symposium on Principles of Programming Languages},
  year = {2003}
}

@article{Curry,
  title={Functionality in Combinatory Logic},
  author = {H. B. Curry},
  journal = {Proceedings of the National Academy of Sciences of the United States of America},
  volume = {20(11)},
  year = {1934},
  pages = {584--590}
}

@incollection{Howard,
  author = {Howard, William A.},
  title = {The formulae-as-types notion of construction},
  editor = {Seldin, Jonathan P. and Hindley, J. Roger},
  booktitle = {To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism},
  publisher = {Academic Press},
  pages = {479--490},
  year = {1980},
  note = {Original paper manuscript from 1969}
}

@inproceedings{HOAS,
 author = {Pfenning, F. and Elliot, C.},
 title = {Higher-order abstract syntax},
 booktitle = {Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation},
 year = {1988},
 pages = {199--208},
} 

@article{HOU,
 author = {G\'erard Huet},
 title = {The undecidability of unification in third order logic},
 journal = {Information and Control},
 voluem = {22(3)},
 year = {1973},
 pages = {257--267}
}

@InBook{TAPLNatDed,
  author       = "Benjamin C. Pierce",
  title        = "Types and Programming Languages",
  year         = "2002",
  publisher    = "MIT Press",
  chapter      = "9.4"
}

@inproceedings{Monads,
 author = {Wadler, Philip},
 title = {The essence of functional programming},
 booktitle = {Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 year = {1992},
} 

@inproceedings{IO,
 author = {Peyton Jones, Simon L. and Wadler, Philip},
 title = {Imperative functional programming},
 booktitle = {Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 year = {1993},
} 

@InProceedings{separation,
  author = 	 {John C. Reynolds},
  title = 	 {Separation Logic: A Logic for Shared Mutable Data Structures},
  booktitle =    {Proceedings of the IEEE Symposium on Logic in Computer Science},
  year = 	 {2002}
}

@article{Okasaki,
 author = {Okasaki, Chris},
 title = {Red-black trees in a functional setting},
 journal = {J. Funct. Program.},
 volume = {9},
 issue = {4},
 year = {1999},
 pages = {471--477},
} 

@Article{DeBruijn,
  author =       "Nicolas G. de Bruijn",
  title =        "Lambda-calculus notation with nameless dummies: a tool for automatic formal manipulation with application to the {Church-Rosser} theorem",
  journal =      "Indag. Math.",
  volume =       "34(5)",
  pages =        "381--392",
  year =         "1972"
}

@INPROCEEDINGS{GirardsParadox,
    author = {Thierry Coquand},
    title = {An Analysis of {Girard's} Paradox},
    booktitle = {Proceedings of the Symposium on Logic in Computer Science},
    year = {1986},
    pages = {227--236}
}

@inproceedings{PCC,
 author = {George C. Necula},
 title = {Proof-carrying code},
 booktitle = {Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 year = {1997},
}

@inproceedings{XCAP,
 author = {Ni, Zhaozhong and Shao, Zhong},
 title = {Certified assembly programming with embedded code pointers},
 booktitle = {Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 year = {2006},
 }

@TechReport{IT,
  title =	 "A Tutorial on Recursive Types in {Coq}",
  author =	 "Eduardo Gim\'enez",
  year =	 "1998",
  month =	 may,
  number =	 "0221",
  institution =	 "INRIA",
}