Publications
HAL
arXiv
SemanticsScholar
CCSB
DBLP
AMiner
CiteSeer
Google
Scopus
Journals
- 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
Encoding of Predicate Subtyping and Proof Irrelevance in the λΠ-calculus Modulo Theory, with Gabriel Hondet, 18 pages, submitted
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, 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.
Formal proofs (see CoLoR)
(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 21 January 2021.
Come back to main page.