An introduction to mathematical logic and type theory-to truth through proof. Computer science and applied mathematics, 1986. ,
The Matita Interactive Theorem Prover, Automated Deduction-CADE-23-23rd International Conference on Automated Deduction, pp.64-69, 2011. ,
FoCaLiZe and Dedukti to the Rescue for Proof Interoperability, Interactive Theorem Proving8th International Conference, pp.131-147, 2017. ,
Foundational Proof Certificates in First-Order Logic, Automated Deduction-CADE-24-24th International Conference on Automated Deduction, vol.7898, pp.162-177, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00906485
An Analysis of Girard's Paradox, Proceedings of the Symposium on Logic in Computer Science (LICS '86), pp.227-236, 1986. ,
Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, Typed Lambda Calculi and Applications, 8th International Conference, vol.4583, pp.102-117, 2007. ,
A Framework for Defining Logics, J. ACM, vol.40, issue.1, pp.143-184, 1993. ,
The OpenTheory Standard Theory Library, Third International Symposium on NASA Formal Methods (NFM 2011), vol.6617, pp.177-191, 2011. ,
Importing HOL Light into Coq, Interactive Theorem Proving, First International Conference, vol.6172, pp.307-322, 2010. ,
Higher-order Abstract Syntax, SIGPLAN Not, vol.23, issue.7, pp.199-208, 1988. ,
A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions, 35th Annual ACM Symposium on Principles of Programming Languages (POPL'08, pp.371-382, 2008. ,
Vérification de typage pour le lambda-Pi-Calcul Modulo : théorie et pratique), Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice, 2015. ,
, The Coq Proof Assistant, version 8.7.1. Available at, 2017.
, Arithmetic library, The Matita development team, 2018.
Interoperability in Dedukti: From the Calculus of Inductive Constructions to an extension of HOL, 2018. ,
Sharing a library between proof assistants: reaching out to the HOL family, 2018. ,