Talks
September 2024: Translating libraries of definitions and theorems between proof systems (invited talk), 15th International Conference on Interactive Theorem Proving, (ITP'24) , Tbilisi, Georgia
August 2024: Interoperability of Proof Systems using Lambdapi (invited lecturer), 14th International School on Rewriting (ISR'24 ), Obergurgl, Austria
July 2024: Translating HOL-Light proofs to Coq , Workshop on Libraries of Digital Math , Trimester Program: "Prospects of Formal Mathematics", Hausdorff Institute for Mathematics, Bonn, Germany [video]
May 2024: Translating HOL-Light proofs to Coq , LPAR'24 , Mauritius
September 2023: Progresses on proof system interoperability (invited talk), 16th Conference on Intelligent Computer Mathematics (CICM'23 ), Cambridge, UK
July 2023: Lambdapi, a proof assistant featuring rewriting (invited talk), IFIP WG 1.6 on rewriting, Rome, Italy
May 2023, Encoding type universes without using matching modulo AC, AIST, Japan
May 2023: Introduction to proof system interoperability, Dedukti and Lambdapi, EuroProofNet workshop, Liège, Belgium, and Chalmers University seminar, Göteborg, Sweden
September 2022: Lectures on λΠ-calculus modulo rewriting and proof system interoperability, VTSA'22 summer school, Saarbrücken, Germany [lecture1] [lecture2]
August 2022, Encoding type universes without using matching modulo AC , 7th International Conference on
Formal Structures for Computation and Deduction, FSCD'22 , Haifa, Israel
June 2022, Introduction to proof system interoperability, the Dedukti language and the Lambdapi tool , 1st Dedukti school , Nantes, France [video]
July 2020, Type safety of rewrite rules
in dependent types , 5th International Conference on Formal
Structures for Computation and Deduction (FSCD'20 ) [video]
June 2020, On the use of confluence in
type theory modulo rewriting (invited talk), 9th International
Workshop on Confluence (IWC'20 ), Paris,
France [video]
December 2019, Dependency Pairs
Termination in Dependent Type Theory Modulo Rewriting (invited
talk), Gunma & Sendai, Japan
June 2019, Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting , Oslo, Norway
July 2017, Gilles Dowek’s
technique for proving the termination of the embedding of HOL in
Dedukti , Chambéry, France
June 2017, Solving constraints in ordinals , LSV annual meeting, Ury, France
October 2016, Using external
provers in proof assistants , seminar on
Universality of proofs , Dagstuhl, Germany
May 2016, Size-based termination
for higher-order rewriting , LIMD seminar, Chambéry, France
March 2016, Size-based termination
for higher-order rewriting , Deducteam seminar, Cachan, France
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 , IFIP WG 1.6 invited talk,
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 , TYPES'07
invited talk, 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
Come back to main page .
