1. P.B. Andrews (1963): A reduction of the axioms for the theory of propositional types. Fundam. Math. 52, pp. 345–350, doi:10.4064/fm-52-3-345-350.
  2. P.B. Andrews (1986): An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press.
  3. A. Assaf (2014): A Calculus of Constructions with explicit subtyping. In: H. Herbelin, P. Letouzey & M. Sozeau: Types, LIPICS 39, pp. 27–46, doi:10.4230/LIPIcs.TYPES.2014.27.
  4. A. Assaf (2015): A framework for defining computational higher-order logics. École polytechnique.
  5. A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek, C. Dubois, F. Gilbert, P. Halmagrand, O. Hermant & R. Saillard (2016): Dedukti: a Logical Framework based on the lambda-Pi-Calculus Modulo Theory. Manuscript.
  6. H. Barendregt (1992): Lambda calculi with types. In: S. Abramsky, D.M. Gabbay & T.S.E. Maibaum: Handbook of Logic in Computer Science 2. Oxford University Press, pp. 117–309.
  7. M. Boespflug (2011): Conception d'un noyau de vérification de preuves pour le lambda-Pi-calcul modulo. École polytechnique.
  8. M. Boespflug & G. Burel (2012): CoqInE : Translating the Calculus of Inductive Constructions into the lambda-Pi-calculus modulo. In: Second International Workshop on Proof Exchange for Theorem Proving, pp. 44–50.
  9. R. Cauderlier (2017): A Rewrite System for Proof Constructivization.
  10. R. Cauderlier & C. Dubois (2017): FoCaLiZe and Dedukti to the Rescue for Proof Interoperability. In: M. Ayala-Rincón & C.A. Muñoz: Interactive Theorem Proving, Lecture Notes in Computer Science 10499. Springer, pp. 131–147, doi:10.1007/11916277_11.
  11. A. Church (1940): A formulation of the simple theory of types. The Journal of Symbolic Logic 5(2), pp. 56–68, doi:10.2307/2371199.
  12. T. Coquand & G. Huet (1988): The Calculus of Constructions. Information and Computation, pp. 95–120, doi:10.1016/0890-5401(88)90005-3.
  13. D. Cousineau & G. Dowek (2007): Embedding Pure Type Systems in the lambda-Pi-calculus modulo. In: S. Ronchi Della Rocca: Typed lambda calculi and applications, Lecture Notes in Computer Science 4583. Springer, pp. 102–117, doi:10.1007/978-3-540-73228-0_9.
  14. G. Dowek (2015): On the definition of the classical connectives and quantifiers. In: E.H. Haeusler, W. de Campos Sanz & B. Lopes: Why is this a Proof?, Festschrift for Luiz Carlos Pereira. College Publications.
  15. G. Dowek, Th. Hardin & C. Kirchner (2001): HOL-lambda-sigma: an intentional first-order expression of higher-order logic. Mathematical Structures in Computer Science 11, pp. 1–25, doi:10.1017/S0960129500003236.
  16. G. Dowek, Th. Hardin & C. Kirchner (2003): Theorem proving modulo. Journal of Automated Reasoning 31, pp. 33–72, doi:10.1023/A:1027357912519.
  17. G. Dowek & B. Werner (2003): Proof normalization modulo. The Journal of Symbolic Logic 68(4), pp. 1289–1316, doi:10.1007/BFb0037116.
  18. H. Friedman (1976): Systems of second-order arithmetic with restricted induction, I, II. The Journal of Symbolic Logic 41(2), pp. 557–559.
  19. H. Geuvers (1993): Logics and Type systems. Nijmegen.
  20. H. Geuvers (1995): The Calculus of Constructions and Higher Order Logic. In: Ph. de Groote: The Curry-Howard isomorphism, Cahiers du Centre de logique 8. Université catholique de Louvain, pp. 139–191.
  21. F. Gilbert (2017): Automated Constructivization of Proofs. In: J. Esparza & A.S. Murawski: Foundations of Software Science and Computation Structures, Lecture notes in computer science 10203. Springer, pp. 480–495, doi:10.1007/978-3-540-71070-7_23.
  22. J.-Y. Girard (1993): On the Unity of Logic. Annals of Pure and Applied Logic 59(3), pp. 201–217, doi:10.1016/0168-0072(93)90093-S.
  23. R. Harper, F. Honsell & G. Plotkin (1993): A framework for defining logics. Journal of the ACM 40(1), pp. 143–184, doi:10.1145/138027.138060.
  24. L. Henkin (1960): On Mathematical Induction. The American Mathematical Monthly 67(4), pp. 323–338, doi:10.2307/2308975.
  25. L. Henkin (1963): A theory of propositional types. Fundam. Math. 52, pp. 323–344, doi:10.4064/fm-52-3-323-344. Errata Ibid., 53, 119, 1964.
  26. B. Huffman & Kunçar (2013): Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL. In: G. Gonthier & M. Norrish: Certified Programs and Proofs, pp. 131–146, doi:10.1007/978-3-319-03545-1_9.
  27. J. Hurd (2011): The OpenTheory standard theory library. In: M. Bobaru, K. Havelund, G.J. Holzmann & R. Joshi: NASA Formal Methods, Lecture Notes in Computer Science 6617. Springer, pp. 177–191, doi:10.1007/3-540-60275-5_76.
  28. F. Kirchner (2006): A Finite First-Order Theory of Classes. In: Th. Altenkirch & C. McBride: Types for Proofs and Programs, Lecture Notes in Computer Science. Springer, pp. 188–202.
  29. A. Leitsch (2015): On proof mining by cut-elimination. In: D. Delahaye & B. Woltzenlogel Paleo: All about Proofs, Proofs for All, Mathematical Logic and Foundations 55. College Publications, pp. 173–200.
  30. B. Nordström, K. Petersson & J.M. Smith (2000): Martin-Löf's type theory. In: S. Abramsky, D.M. Gabbay & T.S.E. Maibaum: Handbook of Logic in Computer Science. Clarendon Press, pp. 1–37.
  31. L.C. Pereira (2017). Personal communication.
  32. D. Prawitz (2015): Classical versus intuitionistic logic. In: E.H. Haeusler, W. de Campos Sanz & B. Lopes: Why is this a Proof?, Festschrift for Luiz Carlos Pereira. College Publications.
  33. R. Saillard (2015): Type Checking in the Lambda-Pi-Calculus Modulo: Theory and Practice. École des Mines.
  34. S.G. Simpson (2009): Subsystems of second-order arithmetic. Cambridge University Press, doi:10.1017/CBO9780511581007.
  35. F. Thiré (2017). Personal communication.
  36. F. Thiré (2017): Sharing Arithmetic Proofs from Dedukti to HOL. Manuscript.
  37. T. Zimmermann & H. Herbelin (2015): Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant. Work in progress session, Conference on Intelligent Computer Mathematics,

Comments and questions to:
For website issues: