A. Assaf, A Framework for Defining Computational Higher-Order Logics, 2015.
URL : https://hal.archives-ouvertes.fr/tel-01235303

A. Assaf and G. Burel, Translating HOL to Dedukti, Proceedings Fourth Workshop on Proof eXchange for Theorem Proving. EPTCS, pp.74-88, 2015.
DOI : 10.4204/EPTCS.186.8

URL : https://hal.archives-ouvertes.fr/hal-01097412

R. Bonichon, D. Delahaye, and D. Doligez, Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs, Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, pp.151-165, 2007.
DOI : 10.1007/978-3-540-75560-9_13

URL : https://hal.archives-ouvertes.fr/inria-00315920

G. Burel, A Shallow Embedding of Resolution and Superposition Proofs into the ??-Calculus Modulo, PxTP 2013. 3rd International Workshop on Proof Exchange for Theorem Proving. EasyChair Proceedings in Computing, pp.43-57, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01126321

R. Cauderlier and C. Dubois, Objects and subtyping in the ??-calculus modulo, Post-proceedings of the 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01126394

R. Cauderlier and P. Halmagrand, Checking Zenon Modulo Proofs in Dedukti, Proceedings 4th Workshop on Proof eXchange for Theorem Proving. EPTCS, pp.57-73, 2015.
DOI : 10.4204/EPTCS.186.7

URL : https://hal.archives-ouvertes.fr/hal-01171360

R. Cauderlier, Object-Oriented Mechanisms for Interoperability between Proof Systems, Conservatoire National des Arts et Métiers
URL : https://hal.archives-ouvertes.fr/tel-01415945

D. Cousineau and G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, Typed Lambda Calculi and Applications, pp.102-117, 2007.
DOI : 10.1007/978-3-540-73228-0_9

D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, and O. Hermant, Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo, pp.274-290, 2013.
DOI : 10.1007/978-3-642-45221-5_20

URL : https://hal.archives-ouvertes.fr/hal-00909784

C. Dubois and F. Pessaux, Termination Proofs for Recursive Functions in FoCaLiZe, Trends in Functional Programming -16th International Symposium, TFP 2015, pp.136-156, 2015.
DOI : 10.1007/978-3-319-39110-6_8

J. Giesl, M. Raffelsieper, P. Schneider-kamp, S. Swiderski, and R. Thiemann, Automated termination proofs for haskell by term rewriting, ACM Transactions on Programming Languages and Systems, vol.33, issue.2, pp.1-739, 2011.
DOI : 10.1145/1890028.1890030

URL : http://repository.tue.nl/711512

W. Kahl, Basic Pattern Matching Calculi: a Fresh View on Matching Failure, Functional and Logic Programming Proceedings of FLOPS 2004, pp.276-290, 2004.
DOI : 10.1007/978-3-540-24754-8_20

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.573.4691

J. W. Klop, V. Van-oostrom, and R. De-vrijer, Lambda calculus with patterns, calculi, Types and Applications: Essays in honour of M. Coppo, M. Dezani-Ciancaglini and S, pp.16-31, 2008.
DOI : 10.1016/j.tcs.2008.01.019

URL : http://doi.org/10.1016/j.tcs.2008.01.019

S. Lucas and R. Peña, Rewriting Techniques for Analysing Termination and Complexity Bounds of SAFE Programs, LOPSTR'08, pp.43-57, 2008.

F. Pessaux, FoCaLiZe: Inside an F-IDE, Proceedings 1st Workshop on Formal Integrated Development Environment , F-IDE 2014, pp.64-78, 2014.
DOI : 10.4204/EPTCS.149.7

URL : https://hal.archives-ouvertes.fr/hal-01203501

P. Jones and S. L. , The Implementation of Functional Programming Languages (Prentice-Hall International Series in Computer Science), 1987.

R. Saillard, Type Checking in the Lambda-Pi-Calculus Modulo: Theory and Practice, p.MINES Paritech, 2015.