@unpublished(assaf_calculus_2014,
 author       = {Ali Assaf},
 year         = {2014},
 title        = {{A calculus of constructions with explicit subtyping}},
 url          = {https://hal.inria.fr/hal-01097401},
 note         = {Accepted in {P}ostproceedings of {Types} 2014},
)
@inproceedings(assaf_conservativity_2015,
 author       = {Ali Assaf},
 year         = {2015},
 title        = {{Conservativity of embeddings in the lambda-{Pi} calculus modulo rewriting}},
 editor       = {Thorsten Altenkirch},
 booktitle    = {International Conference on Typed Lambda Calculi and Applications (TLCA)},
 series       = {LIPIcs},
 volume       = {38},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
 pages        = {31--44},
 doi          = {10.4230/LIPIcs.TLCA.2015.31},
)
@unpublished(assaf_translating_2014,
 author       = {Ali Assaf and Guillaume Burel},
 year         = {2015},
 title        = {{Translating {HOL} to {Dedukti}}},
 url          = {https://hal.inria.fr/hal-01097412},
 note         = {Accepted in {PxTP} 2015},
)
@incollection(barendregt_lambda_1992,
 author       = {Henk Barendregt},
 year         = {1992},
 title        = {Lambda calculi with types},
 editor       = {Samson Abramsky and Dov M. Gabbay and Thomas S. E. Maibaum},
 booktitle    = {Handbook of {Logic} in {Computer} {Science}},
 volume       = {2},
 publisher    = {Oxford University Press},
 pages        = {117--309},
)
@inproceedings(boespflug_lambda-pi-calculus_2012,
 author       = {M. Boespflug and Q. Carbonneaux and O. Hermant},
 year         = {2012},
 title        = {The lambda-{Pi}-calculus modulo as a universal proof language},
 booktitle    = {Proof {Exchange} for {Theorem} {Proving} - {Second} {International} {Workshop}, {PxTP} 2012},
 pages        = {28--43},
)
@inproceedings(boespflug_coqine_2012,
 author       = {Mathieu Boespflug and Guillaume Burel},
 year         = {2012},
 title        = {{{CoqInE}: Translating the calculus of inductive constructions into the $\lambda\Pi $-calculus modulo}},
 booktitle    = {{Proof {Exchange} for {Theorem} {Proving} - {Second} {International} {Workshop}, {PxTP} 2012}},
 pages        = {44},
)
@inproceedings(zenon,
 author       = {Richard Bonichon and David Delahaye and Damien Doligez},
 year         = {2007},
 title        = {{{Zenon}: An Extensible Automated Theorem Prover Producing Checkable Proofs}},
 booktitle    = {Logic for Programming Artificial Intelligence and Reasoning (LPAR)},
 series       = {LNCS/LNAI},
 volume       = {4790},
 publisher    = {Springer},
 pages        = {151--165},
 doi          = {10.1007/978-3-540-75560-9\_13},
)
@inproceedings(burel_shallow_2013,
 author       = {Guillaume Burel},
 year         = {2013},
 title        = {A Shallow Embedding of Resolution and Superposition Proofs into the $\lambda${$\Pi$}-Calculus Modulo},
 editor       = {Jasmin Christian Blanchette and Josef Urban},
 booktitle    = {{Proof {Exchange} for {Theorem} {Proving} - {Third} {International} {Workshop}, {PxTP} 2013}},
 series       = {EPiC},
 volume       = {14},
 publisher    = {{EasyChair}},
 pages        = {43--57},
)
@unpublished(Zenon-Modulo,
 author       = {Rapha{\"e}l Cauderlier and Pierre Halmagrand},
 year         = {2015},
 title        = {Checking {Zenon Modulo} proofs in {Dedukti}},
 note         = {Accepted in {PxTP} 2015},
)
@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    = {Typed Lambda Calculi and Applications, 8th International Conference, {TLCA} 2007, {P}aris, {F}rance, June 26-28, 2007, Proceedings},
 series       = {{LNCS}},
 volume       = {4583},
 publisher    = {Springer},
 pages        = {102--117},
 doi          = {10.1007/978-3-540-73228-0\_9},
)
@incollection(delahaye_zenon_2013,
 author       = {David Delahaye and Damien Doligez and Fr\'ed\'eric Gilbert and Pierre Halmagrand and Olivier Hermant},
 year         = {2013},
 title        = {Zenon Modulo: When {A}chilles Outruns the Tortoise Using Deduction Modulo},
 editor       = {Ken McMillan and Aart Middeldorp and Andrei Voronkov},
 booktitle    = {{LPAR}},
 series       = {{LNCS}},
 volume       = {8312},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {274--290},
 doi          = {10.1007/978-3-642-45221-5\_20},
)
@techreport(dowek_models_2014,
 author       = {Gilles Dowek},
 year         = {2014},
 title        = {Models and termination of proof-reduction in the lambda-{Pi}-calculus modulo theory},
 type         = {Technical report},
 institution  = {Inria},
 address      = {Paris},
 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(harper_framework_1993,
 author       = {Robert Harper and Furio Honsell and Gordon Plotkin},
 year         = {1993},
 title        = {A framework for defining logics},
 journal      = {Journal of the ACM},
 volume       = {40},
 number       = {1},
 pages        = {143--184},
 doi          = {10.1145/138027.138060},
)
@incollection(harrison_hol_2009,
 author       = {John Harrison},
 year         = {2009},
 title        = {{HOL} {Light}: An Overview},
 editor       = {Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel},
 booktitle    = {Theorem Proving in Higher Order Logics},
 series       = {{LNCS}},
 volume       = {5674},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {60--66},
 doi          = {10.1007/978-3-642-03359-9\_4},
)
@article(horozalrabe2011,
 author       = {Fulya Horozal and Florian Rabe},
 year         = {2011},
 title        = {{Representing model theory in a type-theoretical logical framework}},
 journal      = {Theoretical Computer Science},
 volume       = {412},
 pages        = {4919--4945},
 doi          = {10.1016/j.tcs.2011.03.022},
)
@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    = {Interactive {Theorem} {Proving}},
 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} {Light} into {Coq}},
 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},
)
@incollection(naumov_hol/nuprl_2001,
 author       = {Pavel Naumov and Mark-Oliver Stehr and Jos\'e Meseguer},
 year         = {2001},
 title        = {The {HOL}/{NuPRL} proof translator},
 editor       = {Richard J. Boulton and Paul B. Jackson},
 booktitle    = {Theorem {Proving} in {Higher} {Order} {Logics}},
 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 Carsten Sch{\"u}rmann},
 year         = {1999},
 title        = {System Description: {Twelf} {\textemdash} A Meta-Logical Framework for Deductive Systems},
 booktitle    = {Automated Deduction {\textemdash} {CADE}-16},
 series       = {{LNCS}},
 volume       = {1632},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {202--206},
 doi          = {10.1007/3-540-48660-7\_14},
)
@inproceedings(saillard_dedukti_2013,
 author       = {Ronan Saillard},
 year         = {2013},
 title        = {Dedukti: a universal proof checker},
 booktitle    = {Foundation of {Mathematics} for {Computer}-{Aided} {Formalization} {Workshop}},
 address      = {Padova},
 url          = {https://hal.inria.fr/hal-00833992},
)
@inproceedings(saillard_towards_2013,
 author       = {Ronan Saillard},
 year         = {2013},
 title        = {{Towards explicit rewrite rules in the $\lambda\Pi $-calculus modulo}},
 booktitle    = {{IWIL} - 10th International Workshop on the Implementation of Logics},
 url          = {https://hal.inria.fr/hal-00921340},
)
@incollection(schurmann_executable_2006,
 author       = {Carsten Sch{\"u}rmann and Mark-Oliver Stehr},
 year         = {2006},
 title        = {An Executable Formalization of the {HOL}/{Nuprl} Connection in the Metalogical Framework Twelf},
 editor       = {Miki Hermann and Andrei Voronkov},
 booktitle    = {Logic for Programming, Artificial Intelligence, and {Reasoning}},
 series       = {{LNCS}},
 volume       = {4246},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {150--166},
 doi          = {10.1007/11916277\_11},
)
@incollection(TPTPderivation,
 author       = {Geoff Sutcliffe and Stephan Schulz and Koen Claessen and Van Gelder, Allen},
 year         = {2006},
 title        = {Using the TPTP Language for Writing Derivations and Finite Interpretations},
 editor       = {Ulrich Furbach and Natarajan Shankar},
 booktitle    = {Automated Reasoning},
 series       = {{LNCS}},
 volume       = {4130},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {67--81},
 doi          = {10.1007/11814771\_7},
)
@manual(coq_development_team_coq_2012,
 author       = {The {Coq} development team},
 year         = {2012},
 title        = {The {Coq} Reference Manual, version 8.4},
 url          = {http://coq.inria.fr/doc},
)