Publications
HAL
arXiv
SemanticsScholar
CCSB
DBLP
Google
Scopus
Orcid
Journals
A modular construction of type theories, with Gilles Dowek, Emilie Grienenberger, Gabriel
Hondet and François Thiré, 28 pages, to appear
in LMCS.- 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.
As editor
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
- 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, accepted at 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.
- 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.
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. SPECIF
2001 PhD Award.
- 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
(Links below give the definitions and statements only. Download CoLoR to see the the 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.
Last updated on 24 March 2023.
Come back to main page.