Publications

HAL  arXiv  SemanticsScholar  CCSB  DBLP  Google  Scopus  Orcid

Submitted

• Towards the Verification of Higher-Order Logic Automated Reasoning, with Melanie Taprogge and Alexander Steen

Journals

• Sharing proofs with predicative theories through universe polymorphic elaboration, with Thiago Felicissimo, 38 pages, accepted for publication in LMCS.
• A modular construction of type theories, with Gilles Dowek, Emilie Grienenberger, Gabriel Hondet and François Thiré, 28 pages, LMCS 19(1), 2023.
• Size-based termination of higher-order rewriting, JFP 28 e11, 75 pages, 2018.
• Termination of rewrite relations on λ-terms based on Girard's notion of reducibility, TCS 611, 37 pages, 2016. Erratum.
• 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. Erratum.
• A document-centered approach for an open CASE environment framework connected with the WWW, SEN 22(2), 6 pages, 1997.

As editor

• 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.

Invited publications

• 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.

Conferences

• Proof Verification with GDV and LambdaPi, It's a Matter of Trust, with Geoff Sutcliffe and Guillaume Burel, 8 pages, FLAIRS'25.
• Translating HOL-Light proofs to Coq, 18 pages. LPAR'24.
• Translating proofs from an impredicative type system to a predicative one, with Thiago Felicissimo and Ashish Kumar Barnawal, 19 pages, CSL'23, LIPIcs 252.
• Encoding type universes without using matching modulo AC, 14 pages, FSCD'22.
• Some axioms for mathematics, with Gilles Dowek, Emilie Grienenberger, Gabriel Hondet and François Thiré, 19 pages, FSCD'21, LIPIcs 195.
• Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-calculus Modulo Theory, with Gabriel Hondet, 18 pages, 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. Erratum.
• 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. [annexes]
• The Calculus of Algebraic Constructions, with J.-P. Jouannaud and M. Okada, RTA'99, LNCS 1631, 15 pages.

Theses

• 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. Version en français. SPECIF 2001 PhD Award. Erratum.
• The Calculus of Algebraic and Inductive Constructions, Master thesis, 35 pages, 1998.

Lecture notes

• Langages formels et automates, 35 pages, 2017-2021.
• Exercices corrigés sur les langages formels et automates, 46 pages, 2017-2021.
• Rewriting theory, 43 pages, 2016-2021.
• Corrected exercices and homeworks on rewriting theory, 55 pages, 2016-2021.
• Notes de révision sur le λ-calcul (leçon 929) pour l'option informatique de l'agrégation de mathématiques, 13 pages.
• Notes de révision sur les théories en logique du 1er order (leçon 924) pour l'option informatique de l'agrégation de mathématiques, 14 pages.
• 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.

Formal proofs

• 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.

Other publications

• 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.