Teaching

• Formal languages and finite automata at the ENSIIE engineering school since 2017
• Rewriting theory at the Parisian Research Master in Informatics (MPRI) since 2016
• Sep 2025: λΠ-calculus modulo rewriting: theory and application to proof systems interoperability, 1st International School on Logical Frameworks and Proof Systems Interoperability, Orsay, France
[lecture 1] [lecture 2] [lecture 3] [lecture 4]
• Aug 2024: Interoperability of Proof Systems using Lambdapi, 14th International School on Rewriting, Obergurgl, Austria
• Sep 22: Lectures on λΠ-calculus modulo rewriting and proof system interoperability at the VTSA'22, Saarbrücken, Germany [lecture1] [lecture2]
• June 22: Introduction to proof system interoperability, Dedukti and Lambdapi at the 1st Dedukti school, Nantes, France [slides] [video]
• Préparation à l'agrégation à l'ENS Paris-Saclay between 2018 and 2021
• Mar 2013: Spring school on formal methods in software engineering (IAMI, Ho Chi Minh City, Vietnam)
  • Elements of mathematics and logic for computer program analysis
  • Introduction to the OCaml programming language
  • Introduction to the Coq proof assistant
• May 2012: Introduction to domain theory and topology (ISCAS, Beijing, China)
• Aug 2010: 2nd Asian-Pacific Summer School on Formal Methods (Beijing, China)
  • Type checking and type inference in the simply-typed lambda-calculus
  • Termination of beta-reduction in the simply-typed lambda-calculus
• Aug 2009: 1st Asian-Pacific Summer School on Formal Methods (Beijing, China)
• Mar 2009: Lectures on the meta-theory of System F (Tsinghua University, Beijing, China)
• Oct 2008 - Feb 2009: Lectures on Coq (Tsinghua University, Beijing, China)
• Mar 2008: Introduction to typed lambda-calculus and logic (Tsinghua University, Beijing, China)
• Jan 1999 - Jun 2001: Teaching assistant in computer science at the Technical Institute of the University of Paris 11 (Orsay, France) on database files management (Cobol and MySQL) and programmation with objects and modules (ADA)
• Oct 1998 - Dec 1998: Teaching assistant in computer science at the University of Paris 11 (Orsay, France) on functional programming
• Sep 1997 - Mar 2001: Examiner in mathematics in the "classes préparatoires" of Paul Valéry, Condorcet and Saint Louis (Paris, France)