Publications
HAL
arXiv
CCSB
DBLP
Microsoft
AMiner
CSDoc
Google
ISI
Scopus
Journals
Size-based termination of
higher-order rewrite systems, submitted, 57 pages, 2015.- Termination of rewrite relations on
λ-terms based on Girard's notion of
reducibility, TCS
611, 37 pages, 2015.
- 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.
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
- 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
Formal proofs (see CoLoR)
- 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
- Notes on the theory of
cardinals, 8 pages, 2015.
- A point on fixpoints in posets,
note, 10 pages, 2014.
- Automated verification of termination
certificates, with K. Q. Ly, note 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, note, 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.
- An Isabelle formalization of
protocol-independent secrecy with an application to e-commerce,
note, 16 pages, 2002.
Last updated on 15 December 2015.
Come back to main page.