Teaching

• Sep-Oct 2024: Rewriting theory at the MPRI
• Sep-Oct 2024: Formal languages and finite automata at the ENSIIE
• Aug 2024: Interoperability of Proof Systems using Lambdapi, 14th International School on Rewriting (invited lecturer), Obergurgl, Austria
• Sep-Oct 2023: Rewriting theory at the MPRI
• Sep-Oct 2023: Formal languages and finite automata at the ENSIIE
• Sep-Oct 2022: Rewriting theory at the MPRI
• Sep-Oct 2022: Formal languages and finite automata at the ENSIIE
• 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]
• Sep-Oct 2021: Rewriting theory at the MPRI
• Sep-Oct 2021: Formal languages and finite automata at the ENSIIE
• Nov 2020 - January 2021: Préparation à l'agrégation à l'ENS Paris-Saclay
• Sep-Nov 2020: Rewriting theory at the MPRI
• Sep-Nov 2020: Formal languages and finite automata at the ENSIIE
• Nov 2019 - Jan 2020: Préparation à l'agrégation à l'ENS Paris-Saclay
• Nov 2019 - Jan 2020: Rewriting theory at the MPRI
• Sep-Nov 2019: Formal languages and finite automata at the ENSIIE
• Nov 2018 - Jan 2019: Rewriting theory at the MPRI
• Nov-Dec 2018: Préparation à l'agrégation à l'ENS Paris-Saclay
• Sep-Nov 2018: Formal languages and finite automata at the ENSIIE
• Nov 2017 - Jan 2018: Rewriting theory at the MPRI
• Sep-Nov 2017: Formal languages and finite automata at the ENSIIE
• Nov 2016 - Jan 2017: Rewriting theory at the MPRI
• 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)