Talks
May 2026: Proof Systems Interoperability, IECL-AHP-LORIA Reflexions Seminar on Proofs, rigor and formalization, Nancy, France
May 2026: Proof Systems Interoperability, research seminar of the Giorgi Nikoladze Scientific Research Center at Kutaisi International University, Georgia
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 .
