1. Peter B. Andrews (1986): An introduction to mathematical logic and type theory - to truth through proof. Computer science and applied mathematics. Academic Press.
  2. Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen & Enrico Tassi (2011): The Matita Interactive Theorem Prover. In: Nikolaj Bjørner & Viorica Sofronie-Stokkermans: Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, Lecture Notes in Computer Science 6803. Springer, pp. 64–69. Available at
  3. Raphaël Cauderlier & Catherine Dubois (2017): FoCaLiZe and Dedukti to the Rescue for Proof Interoperability. In: Mauricio Ayala-Rincón & César A. Muñoz: Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, Lecture Notes in Computer Science 10499. Springer, pp. 131–147. Available at
  4. Zakaria Chihani, Dale Miller & Fabien Renaud (2013): Foundational Proof Certificates in First-Order Logic. In: Maria Paola Bonacina: Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, Lecture Notes in Computer Science 7898. Springer, pp. 162–177. Available at
  5. Thierry Coquand (1986): An Analysis of Girard's Paradox. In: Proceedings of the Symposium on Logic in Computer Science (LICS '86), Cambridge, Massachusetts, USA, June 16-18, 1986. IEEE Computer Society, pp. 227–236.
  6. 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, Lecture Notes in Computer Science 4583. Springer, pp. 102–117. Available at
  7. Robert Harper, Furio Honsell & Gordon D. Plotkin (1993): A Framework for Defining Logics. J. ACM 40(1), pp. 143–184. Available at
  8. Joe Hurd (2011): The OpenTheory Standard Theory Library. In: Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann & Rajeev Joshi: Third International Symposium on NASA Formal Methods (NFM 2011), Lecture Notes in Computer Science 6617. Springer, pp. 177–191. Available at
  9. Chantal Keller & Benjamin Werner (2010): Importing HOL Light into Coq. In: Matt Kaufmann & Lawrence C. Paulson: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, Lecture Notes in Computer Science 6172. Springer, pp. 307–322. Available at
  10. F. Pfenning & C. Elliott (1988): Higher-order Abstract Syntax. SIGPLAN Not. 23(7), pp. 199–208. Available at
  11. Brigitte Pientka (2008): A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In: 35th Annual ACM Symposium on Principles of Programming Languages (POPL'08). ACM, pp. 371–382. Available at
  12. Ronan Saillard (2015): Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice. (Vérification de typage pour le lambda-Pi-Calcul Modulo : théorie et pratique). Mines ParisTech, France. Available at
  13. The Coq Development Team (2017): The Coq Proof Assistant, version 8.7.1. Available at
  14. The Matita development team (2018): Arithmetic library. Available at
  15. François Thiré (2018): Interoperability in Dedukti: From the Calculus of Inductive Constructions to an extension of HOL..
  16. François Thiré (2018): Sharing a library between proof assistants: reaching out to the HOL family..

Comments and questions to:
For website issues: