@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.4",
  year = 2012,
  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",
}

@inproceedings{BigStep,
 author = {Xavier Leroy and Herv\'e Grall},
 title = {Coinductive big-step operational semantics},
 year = {2006},
 booktitle = {Proceedings of the 15th European Symposium on Programming}
}

@InBook{WinskelDomains,
  author       = "Glynn Winskel",
  title        = "The Formal Semantics of Programming Languages",
  year         = "1993",
  publisher    = "MIT Press",
  chapter      = "8"
}

@article{Capretta,
  author     = {Venanzio Capretta},
  title      = {General Recursion via Coinductive Types},
  journal    = {Logical Methods in Computer Science},
  volume     = 1,
  number     = 2,
  year       = 2005,
  pages      = {1--18},
}

@inproceedings{Megacz,
 author = {Adam Megacz},
 title = {A coinductive monad for prop-bounded recursion},
 booktitle =   {Proceedings of the {ACM} Workshop Programming
                Languages meets Program Verification},
 pages = {11--20},
 year = {2007},
}

@inproceedings{modules,
 author = {MacQueen, David},
 title = {Modules for {Standard ML}},
 booktitle = {Proceedings of the 1984 ACM Symposium on LISP and Functional Programming},
 year = {1984},
 pages = {198--207},
} 

@inproceedings{typeclasses,
 author = {Wadler, P. and Blott, S.},
 title = {How to make ad-hoc polymorphism less ad hoc},
 booktitle = {Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 year = {1989},
 pages = {60--76},
} 

@inproceedings{reflection,
  author    = {Boutin, Samuel},
  title     = {Using reflection to build efficient and certified decision procedures},
  booktitle = {Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software},
  year      = {1997},
}

@inproceedings{JMeq,
  author = {McBride, Conor},
  title = {Elimination with a Motive},
  booktitle = {Proceedings of the International Workshop on Types for Proofs and Programs},
  year = {2000},
  pages = {197--216}
}

@phdthesis{AxiomK,
  author = {Thomas Streicher},
  title = {Semantical Investigations into Intensional Type Theory},
  type = {Habilitationsschrift},
  school = {LMU M\"unchen},
  year= {1993}
}

@article{BGB,
 author = {Geoffrey Washburn and Stephanie Weirich},
 title = {Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism},
 journal = {J. Funct. Program.},
 volume = {18},
 number = {1},
 year = {2008},
 pages = {87--140},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
 }

@InProceedings{PhoasICFP08,
author = {Adam Chlipala},
title = {Parametric Higher-Order Abstract Syntax for Mechanized Semantics},
booktitle = {Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming},
year = {2008},
pages = {143--156}
}

@article{parametricity,
 author = {Reynolds, J.C.},
 year = {1983},
 title = {Types, abstraction, and parametric polymorphism},
 journal = {Information Processing},
 pages = {513--523}
}

@InProceedings{CompilerPOPL10,
author = {Adam Chlipala},
title = {A Verified Compiler for an Impure Functional Language},
booktitle = {Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
year = {2010},
}

@inproceedings{Isar,
 author = {Wenzel, Markus},
 title = {Isar - A Generic Interpretative Approach to Readable Formal Proof Documents},
 booktitle = {Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics},
 year = {1999},
} 

@article{continuations,
 author = {Reynolds, John C.},
 title = {The discoveries of continuations},
 journal = {Lisp Symb. Comput.},
 issue_date = {Nov. 1993},
 volume = {6},
 number = {3-4},
 month = nov,
 year = {1993},
 issn = {0892-4635},
 pages = {233--248},
 numpages = {16},
 url = {http://dx.doi.org/10.1007/BF01019459},
 doi = {10.1007/BF01019459},
 acmid = {198114},
 publisher = {Kluwer Academic Publishers},
 address = {Hingham, MA, USA},
 keywords = {continuation, continuation-passing style, semantics},
}

@article{unification,
 author = {Robinson, J. A.},
 title = {A Machine-Oriented Logic Based on the Resolution Principle},
 journal = {J. ACM},
 issue_date = {Jan. 1965},
 volume = {12},
 number = {1},
 month = jan,
 year = {1965},
 issn = {0004-5411},
 pages = {23--41},
 numpages = {19},
 url = {http://doi.acm.org/10.1145/321250.321253},
 doi = {10.1145/321250.321253},
 acmid = {321253},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@ARTICLE{whyfp,
    author = {John Hughes},
    title = {Why Functional Programming Matters},
    journal = {The Computer Journal},
    year = {1984},
    volume = {32},
    pages = {98--107}
}

@Book{Prolog,
  author       = "Leon Sterling and Ehud Shapiro",
  title        = "The Art of Prolog, 2nd Edition",
  year         = "1994",
  publisher    = "MIT Press"
}

@Book{LogicProgramming,
  author       = "John W. Lloyd",
  title        = "Foundations of Logic Programming, 2nd Edition",
  year         = "1987",
  publisher    = "Springer"
}

@InBook{deriving,
  title =	 "Haskell 98 Language and Libraries: The Revised Report",
  author =	 "Simon {Peyton Jones} and Lennart Augustsson and Dave Barton and Brian Boutel and Warren Burton and Joseph Fasel and Kevin Hammond and Ralf Hinze and Paul Hudak and John Hughes and Thomas Johnsson and Mark Jones and John Launchbury and Erik Meijer and John Peterson and Alastair Reid and Colin Runciman and Philip Wadler",
  year =	 "1998",
  chapter =      "4.3.3",
  url =          {http://www.haskell.org/onlinereport/decls.html#derived-decls}
}