@book(andrews_introduction_1986,
 author       = {Peter~B. Andrews},
 year         = {1986},
 title        = {An introduction to mathematical logic and type theory: to truth through proof},
 publisher    = {Academic Press Professional, Inc.},
 address      = {San Diego, {CA}, {USA}},
)
@inproceedings(appel_foundational_2001,
 author       = {Andrew~W. Appel},
 year         = {2001},
 title        = {Foundational Proof-Carrying Code},
 booktitle    = {{LICS}},
 publisher    = {{IEEE} Computer Society},
 address      = {Washington, {DC}, {USA}},
 pages        = {247\IeC{\textendash}256},
 doi          = {10.1109/LICS.2001.932501},
)
@unpublished(assaf_conservativity_2013,
 author       = {Ali Assaf},
 year         = {2015},
 title        = {Conservativity of embeddings in the lambda-{P}i calculus modulo rewriting},
 url          = {https://hal.archives-ouvertes.fr/hal-01084165},
 note         = {To appear in TLCA 2015},
)
@unpublished(assaf_mixing_2015,
 author       = {Ali Assaf and Rapha{\"e}l Cauderlier},
 year         = {2015},
 title        = {{Mixing HOL and Coq in Dedukti (Rough Diamond)}},
 url          = {https://hal.inria.fr/hal-01141789},
 note         = {To appear in PxTP 2015},
)
@book(barendregt_lambda_1992,
 author       = {H.~P. Barendregt},
 year         = {1992},
 title        = {Lambda Calculi with Types, Handbook of Logic in Computer Science Vol. {II}},
 publisher    = {Oxford University Press},
)
@book(beeson_foundations_1985,
 author       = {Michael Beeson},
 year         = {1985},
 title        = {Foundations of Constructive Mathematics},
 publisher    = {Springer-Verlag},
 doi          = {10.1007/978-3-642-68952-9},
)
@inproceedings(boespflug_coqine:_2012,
 author       = {M.~Boespflug and G.~Burel},
 year         = {2012},
 title        = {{CoqInE:} Translating the calculus of inductive constructions into the lambda-Pi-calculus modulo},
 booktitle    = {{PxTP}},
 pages        = {44--50},
)
@inproceedings(boespflug_lambda-pi-calculus_2012,
 author       = {M.~Boespflug and Q.~Carbonneaux and O.~Hermant},
 year         = {2012},
 title        = {The lambda-{{P}i-calculus} modulo as a universal proof language},
 booktitle    = {{PxTP}},
 pages        = {28--43},
)
@incollection(chihani_foundational_2013,
 author       = {Zakaria Chihani and Dale Miller and Fabien Renaud},
 year         = {2013},
 title        = {Foundational proof certificates in first-order Logic},
 editor       = {Maria~Paola Bonacina},
 booktitle    = {Automated {Deduction} {\textendash} {CADE}-24},
 series       = {Lecture {Notes} in {Computer} {Science}},
 volume       = {7898},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {162--177},
 doi          = {10.1007/978-3-642-38574-2\_11},
)
@article(church_formulation_1940,
 author       = {Alonzo Church},
 year         = {1940},
 title        = {A formulation of the simple theory of types},
 journal      = {Journal of Symbolic Logic},
 volume       = {5},
 number       = {02},
 pages        = {56--68},
 doi          = {10.2307/2266170},
)
@incollection(cousineau_embedding_2007,
 author       = {Denis Cousineau and Gilles Dowek},
 year         = {2007},
 title        = {Embedding Pure Type Systems in the Lambda-{P}i-Calculus Modulo},
 editor       = {Simona Ronchi~Della Rocca},
 booktitle    = {{TLCA}},
 series       = {{LNCS}},
 volume       = {4583},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {102--117},
 doi          = {10.1007/978-3-540-73228-0\_9},
)
@unpublished(dowek_models_2014,
 author       = {Gilles Dowek},
 year         = {2014},
 title        = {Models and termination of proof-reduction in the {$\lambda\Pi $}-calculus modulo theory},
 url          = {https://who.rocq.inria.fr/Gilles.Dowek/Publi/superpi.pdf},
)
@phdthesis(geuvers_logics_1993,
 author       = {Herman Geuvers},
 year         = {1993},
 title        = {Logics and type systems},
 type         = {{PhD} thesis},
 school       = {University of Nijmegen},
)
@article(geuvers_logical_1999,
 author       = {Herman Geuvers and Erik Barendsen},
 year         = {1999},
 title        = {Some logical and syntactical observations concerning the first-order dependent type system lambda-{{P}}},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {9},
 number       = {04},
 pages        = {335--359},
 doi          = {10.1017/S0960129599002856},
)
@article(hales_jordan_2007,
 author       = {Thomas~C. Hales},
 year         = {2007},
 title        = {The {{J}ordan} Curve Theorem, Formally and Informally},
 journal      = {American Mathematical Monthly},
 volume       = {114},
 number       = {10},
 pages        = {882--894},
)
@incollection(hales_revision_2011,
 author       = {Thomas~C. Hales and John Harrison and Sean {McLaughlin} and Tobias Nipkow and Steven Obua and Roland Zumkeller},
 year         = {2011},
 title        = {A Revision of the Proof of the {{K}epler} Conjecture},
 editor       = {Jeffrey~C. Lagarias},
 booktitle    = {The Kepler Conjecture},
 publisher    = {Springer New York},
 pages        = {341--376},
 doi          = {10.1007/978-1-4614-1129-1\_9},
)
@article(harper_framework_1993,
 author       = {Robert Harper and Furio Honsell and Gordon Plotkin},
 year         = {1993},
 title        = {A framework for defining logics},
 journal      = {J. {ACM}},
 volume       = {40},
 number       = {1},
 pages        = {143\IeC{\textendash}184},
 doi          = {10.1145/138027.138060},
)
@incollection(hurd_opentheory_2011,
 author       = {Joe Hurd},
 year         = {2011},
 title        = {The {OpenTheory} Standard Theory Library},
 editor       = {Mihaela Bobaru and Klaus Havelund and Gerard~J. Holzmann and Rajeev Joshi},
 booktitle    = {NFM},
 series       = {{LNCS}},
 volume       = {6617},
 publisher    = {Springer},
 pages        = {177--191},
 doi          = {10.1007/978-3-642-20398-5\_14},
)
@incollection(kaliszyk_scalable_2013,
 author       = {Cezary Kaliszyk and Alexander Krauss},
 year         = {2013},
 title        = {Scalable {LCF}-Style Proof Translation},
 editor       = {Sandrine Blazy and Paulin-Mohring, Christine and David Pichardie},
 booktitle    = {{ITP}},
 series       = {{LNCS}},
 volume       = {7998},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {51--66},
 doi          = {10.1007/978-3-642-39634-2\_7},
)
@incollection(keller_importing_2010,
 author       = {Chantal Keller and Benjamin Werner},
 year         = {2010},
 title        = {Importing {HOL} {L}ight into {C}oq},
 editor       = {Matt Kaufmann and Lawrence~C. Paulson},
 booktitle    = {ITP},
 series       = {{LNCS}},
 volume       = {6172},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {307--322},
 doi          = {10.1007/978-3-642-14052-5\_22},
)
@article(miller_unification_1991,
 author       = {Dale Miller},
 year         = {1991},
 title        = {Unification of simply typed lambda-terms as logic programming},
 journal      = {Technical Reports (CIS)},
)
@phdthesis(miller_proofs_2004,
 author       = {Dale~A. Miller},
 year         = {2004},
 title        = {Proofs in higher-order logic},
 school       = {University of Pennsylvania},
)
@incollection(naumov_hol/nuprl_2001,
 author       = {Pavel Naumov and Mark-Oliver Stehr and Jos\IeC{\'e} Meseguer},
 year         = {2001},
 title        = {The {HOL}/{NuPRL} Proof Translator},
 editor       = {Richard~J. Boulton and Paul~B. Jackson},
 booktitle    = {{TPHOLs}},
 series       = {{LNCS}},
 volume       = {2152},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {329--345},
 doi          = {10.1007/3-540-44755-5\_23},
)
@incollection(obua_importing_2006,
 author       = {Steven Obua and Sebastian Skalberg},
 year         = {2006},
 title        = {Importing {HOL} into {Isabelle/HOL}},
 editor       = {Ulrich Furbach and Natarajan Shankar},
 booktitle    = {Automated Reasoning},
 series       = {{LNCS}},
 volume       = {4130},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {298--302},
 doi          = {10.1007/11814771\_27},
)
@incollection(pfenning_system_1999,
 author       = {Frank Pfenning and Sch\IeC{\"u}rmann, Carsten},
 year         = {1999},
 title        = {System Description: Twelf \IeC{\textemdash} A Meta-Logical Framework for Deductive Systems},
 booktitle    = {{CADE-16}},
 series       = {{LNCS}},
 volume       = {1632},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {202--206},
 doi          = {10.1007/3-540-48660-7\_14},
)
@article(rabe_representing_2010,
 author       = {Florian Rabe},
 year         = {2010},
 title        = {Representing {I}sabelle in {LF}},
 journal      = {{EPTCS}},
 volume       = {34},
 pages        = {85--99},
 doi          = {10.4204/EPTCS.34.8},
 note         = {{arXiv}: 1009.2794},
)
@article(rabe_scalable_2011,
 author       = {Florian Rabe and Michael Kohlhase},
 year         = {2013},
 title        = {A scalable module system},
 journal      = {Inf. Comput.},
 volume       = {230},
 pages        = {1--54},
 doi          = {10.1016/j.ic.2013.06.001},
)
@incollection(schurmann_executable_2006,
 author       = {Sch\IeC{\"u}rmann, Carsten and Mark-Oliver Stehr},
 year         = {2006},
 title        = {An Executable Formalization of the {HOL/Nuprl} Connection in the Metalogical Framework {T}welf},
 editor       = {Miki Hermann and Andrei Voronkov},
 booktitle    = {{LPAR}},
 series       = {{LNCS}},
 volume       = {4246},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {150--166},
 doi          = {10.1007/11916277\_11},
)
@article(wiedijk_qed_2007,
 author       = {Freek Wiedijk},
 year         = {2007},
 title        = {The {QED} manifesto revisited},
 journal      = {Studies in Logic, Grammar and Rhetoric},
 volume       = {10},
 number       = {23},
 pages        = {121--133},
)