A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek et al., 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

R. Blanco, Applications for Foundational Proof Certificates in theorem proving, 2017.

R. Blanco, Z. Chihani, and D. Miller, 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

Z. Chihani, D. Miller, and F. Renaud, 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

C. Dunchev, F. Guidi, C. Sacerdoti-coen, and E. Tassi, ELPI: fast, embeddable, ?Prolog interpreter, Logic for Programming, Artificial Intelligence, and Reasoning -20th International Conference, vol.9450, pp.460-468, 2015.

F. Guidi, C. Sacerdoti-coen, and E. Tassi, 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

Q. Heath and D. Miller, 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

Q. Heath and D. Miller, 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

S. Lengrand, R. Dyckhoff, and J. Mckinna, 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

D. Miller, 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

D. Miller and G. Nadathur, Programming with Higher-Order Logic, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00776197

E. Tassi, 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

E. Tassi, Coq plugin embedding ELPI, 2020.