@techreport(fil:00,
 author       = "Jean-Christophe Filli\^atre",
 year         = "2000",
 title        = "{Design of a proof assistant: Coq version 7}",
 type         = "{Research Report}",
 number       = "1369",
 institution  = "{LRI, Universit\'e Paris Sud}",
)
@inproceedings(geu:kre:mck:wie:10,
 author       = "Herman Geuvers and Robbert Krebbers and James McKinna and Freek Wiedijk",
 year         = "2010",
 title        = "{Pure Type Systems without Explicit Contexts}",
 editor       = "Karl Crary and Marino Miculan",
 booktitle    = "{Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice}",
 series       = "{Electronic Proceedings in Theoretical Computer Science}",
 volume       = "34",
 pages        = "53--67",
 doi          = "10.4204/EPTCS.34.6",
)
@book(gor:mel:93,
 editor       = "Mike Gordon and Tom Melham",
 year         = "1993",
 title        = "Introduction to HOL",
 publisher    = "Cambridge University Press",
 address      = "Cambridge",
)
@book(gor:mil:wad:79,
 author       = "Mike Gordon and Robin Milner and Christopher Wadsworth",
 year         = "1979",
 title        = "Edinburgh LCF: A Mechanised Logic of Computation",
 series       = "LNCS",
 volume       = "78",
 publisher    = "Springer Verlag",
 address      = "Berlin, Heidelberg, New York",
)
@article(hal:07,
 author       = "Tom Hales",
 year         = "2007",
 title        = "{The Jordan Curve Theorem, Formally and Informally}",
 journal      = "The American Mathematical Monthly",
 volume       = "114",
 pages        = "882--894",
)
@inproceedings(har:96:3,
 author       = "John Harrison",
 year         = "1996",
 title        = "{HOL Light: A Tutorial Introduction}",
 editor       = "Mandayam Srivas and Albert Camilleri",
 booktitle    = "Proceedings of the First International Conference on Formal Methods in Computer-Aided Design ({FMCAD}'96)",
 series       = "LNCS",
 volume       = "1166",
 publisher    = "Springer-Verlag",
 pages        = "265--269",
 doi          = "10.1007/BFb0031814",
)
@inproceedings(har:99,
 author       = "John Harrison",
 year         = "1999",
 title        = "{A Machine-Checked Theory of Floating Point Arithmetic}",
 editor       = "Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Thery",
 booktitle    = "Theorem Proving in Higher Order Logics: {TPHOLs} '99",
 series       = "LNCS",
 volume       = "1690",
 pages        = "113--130",
 doi          = "10.1007/3-540-48256-3_9",
)
@manual(har:00,
 author       = "John Harrison",
 year         = "2000",
 title        = "The HOL Light manual (1.1)",
)
@inproceedings(har:06:1,
 author       = "John Harrison",
 year         = "2006",
 title        = "{Floating-Point Verification using Theorem Proving}",
 booktitle    = "Proceedings of SFM 2006, the 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems",
 series       = "LNCS",
 volume       = "2965",
 pages        = "211--242",
 doi          = "10.1007/11757283_8",
)
@inproceedings(har:06,
 author       = "John Harrison",
 year         = "2006",
 title        = "{Towards self-verification of HOL Light}",
 editor       = "Ulrich Furbach and Natarajan Shankar",
 booktitle    = "Proceedings of the Third International Joint Conference IJCAR 2006",
 series       = "LNCS",
 volume       = "4130",
 publisher    = "Springer",
 address      = "Seattle, WA",
 pages        = "177--191",
 doi          = "10.1007/11814771_17",
)
@inproceedings(har:08,
 author       = "John Harrison",
 year         = "2008",
 title        = "{Formalizing an Analytic Proof of the Prime Number Theorem}",
 editor       = "R. Boulton and J. Hurd and K. Slind",
 booktitle    = "{Tools and Techniques for Verification of System Infrastructure}",
 publisher    = "The Royal Society",
 pages        = "243--261",
 doi          = "10.1007/s10817-009-9145-6",
)
@book(lei:69,
 author       = "A. C. Leisenring",
 year         = "1969",
 title        = "Mathematical logic and Hilbert's {$\varepsilon $}-symbol",
 publisher    = "Macdonald",
)
@manual(ler:08,
 author       = "Xavier Leroy",
 year         = "2008",
 title        = "{The Objective Caml system release 3.11, Documentation and user's manual}",
)
@book(wen:02:1,
 author       = "Makarius Wenzel",
 year         = "2002",
 title        = "The Isabelle/Isar Reference Manual",
 publisher    = "TU M{\"u}nchen",
)
@unpublished(wie:10,
 author       = "Freek Wiedijk",
 year         = "2010",
 title        = "{Pollack-inconsistency}",
 note         = "To be published in UITP 2010",
)