1. Ali Assaf (2014): A calculus of constructions with explicit subtyping. Available at Accepted in Postproceedings of Types 2014.
  2. Ali Assaf (2015): Conservativity of embeddings in the lambda-Pi calculus modulo rewriting. In: Thorsten Altenkirch: International Conference on Typed Lambda Calculi and Applications (TLCA), LIPIcs 38. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 31–44, doi:10.4230/LIPIcs.TLCA.2015.31.
  3. Ali Assaf & Guillaume Burel (2015): Translating HOL to Dedukti. Available at Accepted in PxTP 2015.
  4. Henk Barendregt (1992): Lambda calculi with types. In: Samson Abramsky, Dov M. Gabbay & Thomas S. E. Maibaum: Handbook of Logic in Computer Science 2. Oxford University Press, pp. 117–309.
  5. M. Boespflug, Q. Carbonneaux & O. Hermant (2012): The lambda-Pi-calculus modulo as a universal proof language. In: Proof Exchange for Theorem Proving - Second International Workshop, PxTP 2012, pp. 28–43.
  6. Mathieu Boespflug & Guillaume Burel (2012): CoqInE: Translating the calculus of inductive constructions into the λΠ-calculus modulo. In: Proof Exchange for Theorem Proving - Second International Workshop, PxTP 2012, pp. 44.
  7. Richard Bonichon, David Delahaye & Damien Doligez (2007): Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs. In: Logic for Programming Artificial Intelligence and Reasoning (LPAR), LNCS/LNAI 4790. Springer, pp. 151–165, doi:10.1007/978-3-540-75560-9_13.
  8. Guillaume Burel (2013): A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo. In: Jasmin Christian Blanchette & Josef Urban: Proof Exchange for Theorem Proving - Third International Workshop, PxTP 2013, EPiC 14. EasyChair, pp. 43–57.
  9. Raphaël Cauderlier & Pierre Halmagrand (2015): Checking Zenon Modulo proofs in Dedukti. Accepted in PxTP 2015.
  10. Denis Cousineau & Gilles Dowek (2007): Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo. In: Simona Ronchi Della Rocca: Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings, LNCS 4583. Springer, pp. 102–117, doi:10.1007/978-3-540-73228-0_9.
  11. David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand & Olivier Hermant (2013): Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo. In: Ken McMillan, Aart Middeldorp & Andrei Voronkov: LPAR, LNCS 8312. Springer Berlin Heidelberg, pp. 274–290, doi:10.1007/978-3-642-45221-5_20.
  12. Gilles Dowek (2014): Models and termination of proof-reduction in the lambda-Pi-calculus modulo theory. Technical report. Inria, Paris. Available at
  13. Herman Geuvers (1993): Logics and type systems. PhD thesis. University of Nijmegen.
  14. Robert Harper, Furio Honsell & Gordon Plotkin (1993): A framework for defining logics. Journal of the ACM 40(1), pp. 143–184, doi:10.1145/138027.138060.
  15. John Harrison (2009): HOL Light: An Overview. In: Stefan Berghofer, Tobias Nipkow, Christian Urban & Makarius Wenzel: Theorem Proving in Higher Order Logics, LNCS 5674. Springer Berlin Heidelberg, pp. 60–66, doi:10.1007/978-3-642-03359-9_4.
  16. Fulya Horozal & Florian Rabe (2011): Representing model theory in a type-theoretical logical framework. Theoretical Computer Science 412, pp. 4919–4945, doi:10.1016/j.tcs.2011.03.022.
  17. Joe Hurd (2011): The OpenTheory Standard Theory Library. In: Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann & Rajeev Joshi: NFM, LNCS 6617. Springer, pp. 177–191, doi:10.1007/978-3-642-20398-5_14.
  18. Cezary Kaliszyk & Alexander Krauss (2013): Scalable LCF-style proof translation. In: Sandrine Blazy, Christine Paulin-Mohring & David Pichardie: Interactive Theorem Proving, LNCS 7998. Springer Berlin Heidelberg, pp. 51–66, doi:10.1007/978-3-642-39634-2_7.
  19. Chantal Keller & Benjamin Werner (2010): Importing HOL Light into Coq. In: Matt Kaufmann & Lawrence C. Paulson: ITP, LNCS 6172. Springer Berlin Heidelberg, pp. 307–322, doi:10.1007/978-3-642-14052-5_22.
  20. Pavel Naumov, Mark-Oliver Stehr & José Meseguer (2001): The HOL/NuPRL proof translator. In: Richard J. Boulton & Paul B. Jackson: Theorem Proving in Higher Order Logics, LNCS 2152. Springer Berlin Heidelberg, pp. 329–345, doi:10.1007/3-540-44755-5_23.
  21. Steven Obua & Sebastian Skalberg (2006): Importing HOL into Isabelle/HOL. In: Ulrich Furbach & Natarajan Shankar: Automated Reasoning, LNCS 4130. Springer Berlin Heidelberg, pp. 298–302, doi:10.1007/11814771_27.
  22. Frank Pfenning & Carsten Schürmann (1999): System Description: Twelf A Meta-Logical Framework for Deductive Systems. In: Automated Deduction CADE-16, LNCS 1632. Springer Berlin Heidelberg, pp. 202–206, doi:10.1007/3-540-48660-7_14.
  23. Ronan Saillard (2013): Dedukti: a universal proof checker. In: Foundation of Mathematics for Computer-Aided Formalization Workshop, Padova. Available at
  24. Ronan Saillard (2013): Towards explicit rewrite rules in the λΠ-calculus modulo. In: IWIL - 10th International Workshop on the Implementation of Logics. Available at
  25. Carsten Schürmann & Mark-Oliver Stehr (2006): An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf. In: Miki Hermann & Andrei Voronkov: Logic for Programming, Artificial Intelligence, and Reasoning, LNCS 4246. Springer Berlin Heidelberg, pp. 150–166, doi:10.1007/11916277_11.
  26. Geoff Sutcliffe, Stephan Schulz, Koen Claessen & Allen Van Gelder (2006): Using the TPTP Language for Writing Derivations and Finite Interpretations. In: Ulrich Furbach & Natarajan Shankar: Automated Reasoning, LNCS 4130. Springer Berlin Heidelberg, pp. 67–81, doi:10.1007/11814771_7.
  27. The Coq development team (2012): The Coq Reference Manual, version 8.4. Available at

Comments and questions to:
For website issues: