Talks
January 2015, The computability path
ordering , LSV Seminar, Cachan, France
November 2014, A point on fixpoints, GT Logique, Algèbre et
Calcul, Chambéry, France
October 2014, A point on
fixpoints , Deducteam seminar, Paris, France
February 2014, Termination of rewrite relations on λ-terms
based on Tait-Girard's notion of computability, Suzhou Institute for
Advanced Study, China
March 2013, On the formalization of
λ-calculus and Tait-Girard's notion of
computability , PR'13 ,
Kanazawa, Japan
November 2012, Termination of rewrite
relations on λ-terms using the notion of computability
closure , Academia Sinica, Taipei, Taiwan
October 2012, Termination of rewrite relations on λ-terms
using the notion of computability closure, Institute of Software of
the Chinese Academy of Sciences, Beijing, China
July 2012, Functions, rewriting and
proofs: termination and certification (habilitation defense),
University Paris 7, France
May 2012, Computability closure: the
Swiss knife of higher-order termination (invited talk), IFIP WG
1.6, Nagoya, Japan
October 2009, Certification of
embedded systems , Workshop on Simulation Based Development of
Certified Embedded Systems, Osaka, Japan
December 2008, Automated
verification of termination certificates , East China Normal
University, Shanghai, China
February 2008, A new generation of
secure proof assistants integrating small proof engines ,
Münich, Germany
October 2007, HORPO with computability
closure : a
reconstruction , LPAR'07 ,
Yerevan, Armenia
June 2007, Computability closure:
ten years later (Jean-Pierre Jouannaud's 60 birthday), ENS Cachan,
France
May 2007, Automated certification
of termination proofs (invited
talk), TYPES'07 ,
Udine, Italy
March 2007, On the implementation of construction functions for
non-free concrete data
types, ESOP'07 , Braga,
Portugal
November 2006, Combining typing and size constraints for checking
the termination of higher-order conditional rewrite
systems, LPAR'06 ,
Phnom Penh, Cambodia
August 2006, Higher-order dependency
pairs, WST'06 ,
Seattle, USA
August 2006, CoLoR: a Coq Library
on Rewriting and
termination , WST'06 ,
Seattle, USA
August 2005, Decidability of type-checking in the Calculus of
Algebraic Constructions with Size
Annotations, CSL'05 ,
Oxford, UK
June 2004, A type-based termination criterion for
dependently-typed higher-order rewrite
systems, RTA'04 , Aachen,
Germany
June 2003, Rewriting modulo in Deduction modulo,
RTA'03 , Valencia,
Spain
June 2003, Inductive types in the Calculus of Algebraic
Constructions, TLCA'03 ,
Valencia, Spain
September 2001, Type theory and rewriting (PhD defense),
University Paris 11, France
June 2001, Definitions by rewriting in the Calculus of
Constructions, LICS'01 ,
Boston, USA
July 2000, Termination and confluence of higher-order rewrite
systems, RTA'00 , Norwich,
UK
July 1999, The Calculus of Algebraic
Constructions, RTA'99 ,
Trento, Italy
September 1998, The Calculus of Algebraic and Inductive
Constructions (master defense), University Paris 7, France
Last updated on 26 November 2015.
Come back to main page .