HAL arXiv SemanticsScholar CCSB DBLP AMiner CiteSeer Google Scopus

- Size-based termination of higher-order rewriting, in JFP, 75 pages, 2018.
- Termination of rewrite relations on λ-terms based on Girard's notion of reducibility, TCS 611, 37 pages, 2016.
- The computability path ordering, with J.-P. Jouannaud and A. Rubio, LMCS 11(4), 45 pages, 2015.
- Argument filterings and usable rules in higher-order rewrite systems, with K. Kusakari and S. Suzuki, IPSJ Transactions on Programming 4(2), 12 pages, 2011.
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates, with A. Koprowski, MSCS 21(4), 30 pages, 2011.
- On the confluence of lambda-calculus with conditional rewriting, with C. Riba and C. Kirchner, TCS 411(37), 43 pages, 2010.
- Static dependency pair method based on strong computability for higher-order rewrite systems, with Y. Isogai, K. Kusakari and M. Sakai, IEICE Transactions on Information and Systems E92-D(10), 9 pages, 2009.
- Inductive types in the Calculus of Algebraic Constructions, Fundamenta Informaticae 65(1-2), 26 pages, 2005.
- Definitions by rewriting in the Calculus of Constructions, MSCS 15(1), 57 pages, 2005.
- Inductive-data-type Systems, with J.-P. Jouannaud and M. Okada, TCS 272, 30 pages, 2002.
- A document-centered approach for an open CASE environment framework connected with the WWW, SEN 22(2), 6 pages, 1997.

- Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'18), EPTCS 274, with Giselle Reis.
- Works in progress and experience reports of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'18), with Giselle Reis.

- The computability path ordering: the end of a quest, with J.-P. Jouannaud and A. Rubio, CSL'08, 17 pages. LNCS 5213.
- Computability closure: ten years later, essay in honour of Jean-Pierre Jouannaud's 60 birthday, LNCS 4600, 21 pages, 2007.
- Higher-order termination: from Kruskal to computability, with J.-P. Jouannaud and A. Rubio, LPAR'06, LNCS 4246, 14 pages.

- Some axioms for mathematics, with Gilles Dowek, Emilie Grienenberger, Gabriel Hondet and François Thiré, 19 pages, to appear in the proceedings of FSCD'21, LIPIcs 195.
- Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-calculus Modulo Theory, with Gabriel Hondet, 18 pages, to appear in the post-proceedings of TYPES'20, LIPIcs 188.
- The new rewriting engine of Dedukti, with Gabriel Hondet, 16 pages, FSCD 2020, LIPIcs 167.
- Type safety of rewrite rules in dependent types, 14 pages, FSCD 2020, LIPIcs 167.
- Ekstrakto: a tool to reconstruct Dedukti proofs from TSTP files, with Mohamed Yacine El Haddad and Guillaume Burel, 9 pages, PxTP'19, EPTCS 301.
- Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting, with Guillaume Genestier and Olivier Hermant, 21 pages, FSCD'19, LIPIcs 131.
- Termination of λΠ modulo rewriting using the size-change principle (work in progress), with Guillaume Genestier, 5 pages, 2018, WST'18.
- First steps towards the certification of an ARM simulator, with J.-F. Monin, X. Shi and F. Tuong, CPP'11, LNCS 7086, 16 pages.
- Designing a CPU model: from a pseudo-formal document to fast code, with C. Helmstetter, V. Joloboff, J.-F. Monin and X. Shi. RAPIDO'11, 6 pages. Best paper award.
- On the relation between sized-types based termination and semantic labelling, with C. Roux, CSL'09, LNCS 5771, 15 pages.
- From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures, with J.-P. Jouannaud and P.-Y. Strub, TCS'08, IFIP 273, 17 pages.
- HORPO with computability closure : a reconstruction, with J.-P. Jouannaud and A. Rubio, LPAR'07, LNCS 4790, 16 pages.
- Building decision procedures in the Calculus of Inductive Constructions, with J.-P. Jouannaud and P.-Y. Strub, CSL'07, LNCS 4646, 15 pages.
- On the implementation of construction functions for non-free concrete data types, with T. Hardin and P. Weis, ESOP'07, LNCS 4421, 15 pages.
- Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems, with C. Riba, LPAR'06, LNCS 4246, 15 pages.
- Higher-order dependency pairs, WST'06, 5 pages.
- CoLoR, a Coq Library on Rewriting and termination, with S. Coupet-Grimal, W. Delobel, S. Hinderer and A. Koprowski, WST'06, 5 pages.
- On the confluence of lambda-calculus with conditional rewriting, with C. Riba and C. Kirchner, FOSSACS'06, LNCS 3921, 15 pages.
- Decidability of type-checking in the Calculus of Algebraic Constructions with Size Annotations, CSL'05, LNCS 3634, 17 pages.
- A type-based termination criterion for dependently-typed higher-order rewrite systems, RTA'04, LNCS 3091, 15 pages.
- Rewriting modulo in Deduction modulo, RTA'03, LNCS 2706, 15 pages.
- Inductive types in the Calculus of Algebraic Constructions, TLCA'03, LNCS 2701, 14 pages.
- Definitions by rewriting in the Calculus of Constructions, LICS'01, 10 pages. Kleene Award for best student paper.
- Termination and confluence of higher-order rewrite systems, RTA'00, LNCS 1833, 15 pages.
- The Calculus of Algebraic Constructions, with J.-P. Jouannaud and M. Okada, RTA'99, LNCS 1631, 15 pages.

- Terminaison des systèmes de réécriture d'ordre supérieur basée sur la notion de clôture de calculabilité, Habilitation thesis, Université Denis Diderot (Paris 7), 55 pages, 2012.
- Type theory and rewriting, Ph.D. thesis, 139 pages, 2001. SPECIF 2001 PhD Award.
- The Calculus of Algebraic and Inductive Constructions, Master thesis, 35 pages, 1998.

- Langages formels et automates, 32 pages, 2018.
- Exercices corrigés sur les langages formels et automates, 42 pages, 2018.
- Rewriting theory, 37 pages, 2016.
- Notes on the theory of cardinals, 8 pages, 2015.
- Elements of mathematics and logic for computer program analysis, 37 pages, 2013.
- Introduction to the OCaml programming language, 10 pages, 2013.
- Introduction to the Coq proof assistant, 6 pages, 2013.
- Introduction to domain theory and topology, 6 pages, 2012.

- Infinite Ramsey theorem, 2015.
- Equivalence of various definitions of α-equivalence, 2013.
- Termination of higher-order rewrite systems based on the notion of computability closure, 2013.
- Tarski's fixpoint theorem, 2013.
- Girard's reducibility candidates, 2012.
- Pure λ-calculus with named variables and explicit α-equivalence, 2012.
- Transitive closure of a finite graph, 2011.
- Semantic labeling, 2009.
- Dependency graph decomposition, 2008.
- First-order term unification, 2008.
- Dependency pairs, 2004.
- Termination of first-order rewrite systems using polynomial interpretations, with S. Hinderer, 2004.

- Note on the operational semantics of Dedukti 2.5, with Guillaume Genestier, 4 pages, 2018.
- A point on fixpoints in posets, 10 pages, 2014.
- Automated verification of termination certificates, with K. Q. Ly, presented at the 15th Vietnamese National Symposium of Selected ICT Problems, 6 pages, 2012.
- SimSoC-Cert: a certified simulator for systems on chip, with C. Helmstetter, V. Joloboff, J.-F. Monin and X. Shi, 4 pages, 2010.
- Argument filterings and usable rules in higher-order rewrite systems, with K. Kusakari and S. Suzuki, IEICE Technical Report SS2010-24, Vol. 110, No. 169, 15 pages, 2010.
- Automated verification of termination certificates, with A. Koprowski, INRIA Research Report 6949, 24 pages, 2009.
- (HO)RPO revisited, INRIA Research report 5972, 23 pages, 2006.
- Prototype d'extension du système Coq. Projet Averroes, lot 5.1, fourniture 3, rapport technique, 8 pages, 2004.
- Proposition d'architecture du moteur de test de conversion. Projet Averroes, lot 5.1, fourniture 2, rapport technique, 7 pages, 2004.
- Définition de la classe de réécriture à intégrer. Projet Averroes, lot 5.1, fourniture 1, rapport technique, 7 pages, 2004.
- An Isabelle formalization of protocol-independent secrecy with an application to e-commerce, 16 pages, 2002.

Last updated on 13 October 2021. Come back to main page.