A Framework for Defining Computational Higher-Order Logics, 2015. ,
URL : https://hal.archives-ouvertes.fr/tel-01235303
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
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
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
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
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
Object-Oriented Mechanisms for Interoperability between Proof Systems, Conservatoire National des Arts et Métiers ,
URL : https://hal.archives-ouvertes.fr/tel-01415945
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
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
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
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
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
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
Rewriting Techniques for Analysing Termination and Complexity Bounds of SAFE Programs, LOPSTR'08, pp.43-57, 2008. ,
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
The Implementation of Functional Programming Languages (Prentice-Hall International Series in Computer Science), 1987. ,
Type Checking in the Lambda-Pi-Calculus Modulo: Theory and Practice, p.MINES Paritech, 2015. ,