@article(Andrews63,
 author       = {P.B. Andrews},
 year         = {1963},
 title        = {A reduction of the axioms for the theory of propositional types},
 journal      = {Fundam. Math.},
 volume       = {52},
 pages        = {345--350},
 doi          = {10.4064/fm-52-3-345-350},
)
@book(Andrewsbook,
 author       = {P.B. Andrews},
 year         = {1986},
 title        = {An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof},
 publisher    = {Academic Press},
)
@inproceedings(Assaf14,
 author       = {A. Assaf},
 year         = {2014},
 title        = {{A {C}alculus of {C}onstructions with explicit subtyping}},
 editor       = {H. Herbelin and P. Letouzey and M. Sozeau},
 booktitle    = {Types},
 series       = {LIPICS},
 volume       = {39},
 pages        = {27--46},
 doi          = {10.4230/LIPIcs.TYPES.2014.27},
)
@phdthesis(Assafthese,
 author       = {A. Assaf},
 year         = {2015},
 title        = {{A framework for defining computational higher-order logics}},
 school       = {{{\'E}cole polytechnique}},
)
@unpublished(expressing,
 author       = {A. Assaf and G. Burel and R. Cauderlier and D. Delahaye and G. Dowek and C. Dubois and F. Gilbert and P. Halmagrand and O. Hermant and R. Saillard},
 year         = {2016},
 title        = {Dedukti: a Logical Framework based on the lambda-{P}i-Calculus Modulo Theory},
 note         = {Manuscript},
)
@incollection(Barendregt1992,
 author       = {H. Barendregt},
 year         = {1992},
 title        = {Lambda calculi with types},
 editor       = {S. Abramsky and D.M. Gabbay and T.S.E. Maibaum},
 booktitle    = {Handbook of {Logic} in {Computer} {Science}},
 volume       = {2},
 publisher    = {Oxford University Press},
 pages        = {117--309},
)
@phdthesis(Boespflug,
 author       = {M. Boespflug},
 year         = {2011},
 title        = {Conception d'un noyau de v\'erification de preuves pour le lambda-Pi-calcul modulo},
 school       = {\'Ecole polytechnique},
)
@inproceedings(BoespflugBurel,
 author       = {M. Boespflug and G. Burel},
 year         = {2012},
 title        = {Coq{I}n{E} : Translating the {C}alculus of {I}nductive {C}onstructions into the lambda-{P}i-calculus modulo},
 booktitle    = {Second International Workshop on Proof Exchange for Theorem Proving},
 pages        = {44--50},
)
@unpublished(Cauderlier,
 author       = {R. Cauderlier},
 year         = {2017},
 title        = {A Rewrite System for Proof Constructivization},
 note         = {{\tt https://who.rocq.inria.fr/Raphael.Cauderlier/constructivization.pdf}},
)
@inproceedings(CauderlierDubois,
 author       = {R. Cauderlier and C. Dubois},
 year         = {2017},
 title        = {FoCaLiZe and {D}edukti to the Rescue for Proof Interoperability},
 editor       = {Ayala-Rinc\'on, M. and Mu\~noz, C.A.},
 booktitle    = {Interactive Theorem Proving},
 series       = {Lecture Notes in Computer Science},
 volume       = {10499},
 publisher    = {Springer},
 pages        = {131--147},
 doi          = {10.1007/11916277_11},
)
@article(Church40,
 author       = {A. Church},
 year         = {1940},
 title        = {A formulation of the simple theory of types},
 journal      = {The Journal of Symbolic Logic},
 volume       = {5},
 number       = {2},
 pages        = {56--68},
 doi          = {10.2307/2371199},
)
@article(CoquandHuet,
 author       = {T. Coquand and G. Huet},
 year         = {1988},
 title        = {The {C}alculus of {C}onstructions},
 journal      = {Information and Computation},
 pages        = {95--120},
 doi          = {10.1016/0890-5401(88)90005-3},
)
@inproceedings(CD,
 author       = {D. Cousineau and G. Dowek},
 year         = {2007},
 title        = {Embedding {P}ure {T}ype {S}ystems in the lambda-{P}i-calculus modulo},
 editor       = {S. Ronchi Della Rocca},
 booktitle    = {Typed lambda calculi and applications},
 series       = {Lecture Notes in Computer Science},
 volume       = {4583},
 publisher    = {Springer},
 pages        = {102--117},
 doi          = {10.1007/978-3-540-73228-0_9},
)
@incollection(DowekLuizCarlos,
 author       = {G. Dowek},
 year         = {2015},
 title        = {On the definition of the classical connectives and quantifiers},
 editor       = {E.H. Haeusler and W. de Campos Sanz and B. Lopes},
 booktitle    = {Why is this a Proof?, Festschrift for Luiz Carlos Pereira},
 publisher    = {College Publications},
)
@article(DHKHOL,
 author       = {G. Dowek and Th. Hardin and C. Kirchner},
 year         = {2001},
 title        = {{HOL}-lambda-sigma: an intentional first-order expression of higher-order logic},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {11},
 pages        = {1--25},
 doi          = {10.1017/S0960129500003236},
)
@article(DHK,
 author       = {G. Dowek and Th. Hardin and C. Kirchner},
 year         = {2003},
 title        = {Theorem proving modulo},
 journal      = {Journal of Automated Reasoning},
 volume       = {31},
 pages        = {33--72},
 doi          = {10.1023/A:1027357912519},
)
@article(DW,
 author       = {G. Dowek and B. Werner},
 year         = {2003},
 title        = {Proof normalization modulo},
 journal      = {The Journal of Symbolic Logic},
 volume       = {68},
 number       = {4},
 pages        = {1289--1316},
 doi          = {10.1007/BFb0037116},
)
@article(Friedman,
 author       = {H. Friedman},
 year         = {1976},
 title        = {Systems of second-order arithmetic with restricted induction, {I}, {II}},
 journal      = {The Journal of Symbolic Logic},
 volume       = {41},
 number       = {2},
 pages        = {557--559},
)
@phdthesis(Geuversthesis,
 author       = {H. Geuvers},
 year         = {1993},
 title        = {Logics and Type systems},
 school       = {Nijmegen},
)
@incollection(Geuvers95,
 author       = {H. Geuvers},
 year         = {1995},
 title        = {The {C}alculus of {C}onstructions and {H}igher {O}rder {L}ogic},
 editor       = {Ph. de Groote},
 booktitle    = {The Curry-Howard isomorphism},
 series       = {Cahiers du Centre de logique},
 volume       = {8},
 publisher    = {Universit\'e catholique de Louvain},
 pages        = {139--191},
)
@inproceedings(Gilbert,
 author       = {F. Gilbert},
 year         = {2017},
 title        = {Automated Constructivization of Proofs},
 editor       = {J. Esparza and A.S. Murawski},
 booktitle    = {Foundations of Software Science and Computation Structures},
 series       = {Lecture notes in computer science},
 volume       = {10203},
 publisher    = {Springer},
 pages        = {480--495},
 doi          = {10.1007/978-3-540-71070-7_23},
)
@article(GirardUnity,
 author       = {J.-Y. Girard},
 year         = {1993},
 title        = {On the Unity of Logic},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {59},
 number       = {3},
 pages        = {201--217},
 doi          = {10.1016/0168-0072(93)90093-S},
)
@article(HHP,
 author       = {R. Harper and F. Honsell and G. 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},
)
@article(Henkininduction,
 author       = {L. Henkin},
 year         = {1960},
 title        = {On Mathematical Induction},
 journal      = {The American Mathematical Monthly},
 volume       = {67},
 number       = {4},
 pages        = {323--338},
 doi          = {10.2307/2308975},
)
@article(Henkin63,
 author       = {L. Henkin},
 year         = {1963},
 title        = {A theory of propositional types},
 journal      = {Fundam. Math.},
 volume       = {52},
 pages        = {323--344},
 doi          = {10.4064/fm-52-3-323-344},
 note         = {Errata Ibid., 53, 119, 1964},
)
@inproceedings(HuffmanKuncar,
 author       = {B. Huffman and Kun\c{c}ar},
 year         = {2013},
 title        = {Lifting and Transfer: A Modular Design for Quotients in {I}sabelle/{HOL}},
 editor       = {G. Gonthier and M. Norrish},
 booktitle    = {Certified Programs and Proofs},
 pages        = {131--146},
 doi          = {10.1007/978-3-319-03545-1_9},
)
@inproceedings(OpenTheory,
 author       = {J. Hurd},
 year         = {2011},
 title        = {The {O}pen{T}heory standard theory library},
 editor       = {M. Bobaru and K. Havelund and G.J. Holzmann and R. Joshi},
 booktitle    = {NASA Formal Methods},
 series       = {Lecture Notes in Computer Science},
 volume       = {6617},
 publisher    = {Springer},
 pages        = {177--191},
 doi          = {10.1007/3-540-60275-5_76},
)
@inproceedings(Kirchnerf,
 author       = {F. Kirchner},
 year         = {2006},
 title        = {A Finite First-Order Theory of Classes},
 editor       = {Th. Altenkirch and C. McBride},
 booktitle    = {Types for Proofs and Programs},
 series       = {Lecture Notes in Computer Science},
 publisher    = {Springer},
 pages        = {188--202},
)
@inproceedings(Leitsch,
 author       = {A. Leitsch},
 year         = {2015},
 title        = {On proof mining by cut-elimination},
 editor       = {D. Delahaye and B. Woltzenlogel Paleo},
 booktitle    = {All about Proofs, Proofs for All},
 series       = {Mathematical Logic and Foundations},
 volume       = {55},
 publisher    = {College Publications},
 pages        = {173--200},
)
@incollection(NPS,
 author       = {B. Nordstr\"om and K. Petersson and J.M. Smith},
 year         = {2000},
 title        = {Martin-{L}\"of's type theory},
 editor       = {S. Abramsky and D.M. Gabbay and T.S.E. Maibaum},
 booktitle    = {Handbook of {Logic} in {Computer} {Science}},
 publisher    = {Clarendon Press},
 pages        = {1--37},
)
@misc(Pereira,
 author       = {L.C. Pereira},
 year         = {2017},
 howpublished = {Personal communication},
)
@incollection(PrawitzLuizCarlos,
 author       = {D. Prawitz},
 year         = {2015},
 title        = {Classical versus intuitionistic logic},
 editor       = {E.H. Haeusler and W. de Campos Sanz and B. Lopes},
 booktitle    = {Why is this a Proof?, Festschrift for Luiz Carlos Pereira},
 publisher    = {College Publications},
)
@phdthesis(Saillard15,
 author       = {R. Saillard},
 year         = {2015},
 title        = {{Type Checking in the Lambda-Pi-Calculus Modulo: Theory and Practice}},
 school       = {{{\'E}cole des Mines}},
)
@book(Simpson,
 author       = {S.G. Simpson},
 year         = {2009},
 title        = {Subsystems of second-order arithmetic},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511581007},
)
@misc(Thiréperso,
 author       = {F. Thir\'e},
 year         = {2017},
 howpublished = {Personal communication},
)
@unpublished(Thiré,
 author       = {F. Thir\'e},
 year         = {2017},
 title        = {Sharing Arithmetic Proofs from {D}edukti to {HOL}},
 note         = {Manuscript},
)
@unpublished(ZimmermannHerbelin,
 author       = {T. Zimmermann and H. Herbelin},
 year         = {2015},
 title        = {Automatic and Transparent Transfer of Theorems along Isomorphisms in the {C}oq Proof Assistant},
 note         = {Work in progress session, Conference on Intelligent Computer Mathematics, {\tt https://hal.archives-ouvertes.fr/hal-01152588/file/paper.pdf}},
)