Expressing theories in the ??-calculus modulo theory and in the Dedukti system, TYPES: Types for Proofs and Programs, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01441751
Applications for Foundational Proof Certificates in theorem proving, 2017. ,
Translating between implicit and explicit versions of proof, Automated Deduction -CADE 26 -26th International Conference on Automated Deduction, vol.10395, pp.255-273, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01645016
A semantic framework for proof evidence, J. of Automated Reasoning, vol.59, issue.3, pp.287-330, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01390912
ELPI: fast, embeddable, ?Prolog interpreter, Logic for Programming, Artificial Intelligence, and Reasoning -20th International Conference, vol.9450, pp.460-468, 2015. ,
Implementing type theory in higher order constraint logic programming, Mathematical Structures in Computer Science, vol.29, issue.8, pp.1125-1150, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-01410567
A framework for proof certificates in finite state exploration, Proceedings of the Fourth Workshop on Proof eXchange for Theorem Proving, number 186 in Electronic Proceedings in Theoretical Computer Science, pp.11-26, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01240172
A proof theory for model checking, J. of Automated Reasoning, vol.63, issue.4, pp.857-885, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-01814006
A focused sequent calculus framework for proof search in pure type systems, Logical Methods in Computer Science, vol.7, issue.1, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-01110478
Proof checking and logic programming, Formal Aspects of Computing, vol.29, issue.3, pp.383-399, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01390901
Programming with Higher-Order Logic, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00776197
Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq, 10th International Conference on Interactive Theorem Proving (ITP 2019), vol.141, pp.1-29, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-01897468
Coq plugin embedding ELPI, 2020. ,