Lectures at Collège de France
Lectures are given and video-recorded in French. An English translation of the slides is provided here a few months later.
- 2023-2024: Control structures: from "goto" to algebraic effects.
- 2023-2024: Structures de contrôle: de "goto" aux effets algébriques.
- 2022-2023: Persistent data structures.
- 2022-2023: Structures de données persistantes.
- 2021-2022: Language-based software security.
- 2021-2022: Sécurité du logiciel: quel rôle pour les langages de programmation?.
- 2020-2021: Program logics: reasoning principles for high-assurance software. See also the companion Coq development.
- 2020-2021: Logiques de programmes: quand la machine raisonne sur ses logiciels.
- 2019-2020: Mechanized semantics: when machines reason about their languages. See also the companion Coq development.
- 2019-2020: Sémantiques mécanisées : quand la machine raisonne sur ses langages. Voir aussi le développement Coq correspondant.
- 2018-2019: Programming = proving? The Curry-Howard correspondence today.
- 2018-2019: Programmer = démontrer? La correspondance de Curry-Howard aujourd'hui.
Graduate courses
I was involved in the MPRI, a research-oriented graduate curriculum in computer science, co-organized by University Paris 7, ENS Paris, ENS Cachan and École Polytechnique.
- Functional programming and type systems, with Didier Rémy, Yann-Régis Gianas and Giuseppe Castagna, MPRI 2-4, 2010-2017.
- Cours de remise à niveau sur Caml et les systèmes de types, MPRI, 2005-2006.
- Typage et programmation, DEA Programmation, 1998-2001.
- Compilation avancée, DEA Programmation, 1995-1997.
Summer schools and tutorials
- Théorie et pratique des effets en OCaml 5 (in French), JFLA, France, 2023.
- Proving the correctness of a compiler. EUTypes 2019 Summer School, North Macedonia, 2019.
- The formal verification of compilers. DeepSpec Summer School, U. Pennsylvania, 2017.
- Mechanized semantics, with applications to program proof and compiler verification. Verification Technology, Systems & Applications summer school, France, 2013.
- Proving a compiler: mechanized verification of program transformations and static analyses. Oregon Programming Languages Summer School, 2010, 2011, and 2012.
- Mechanized semantics, with applications to program proof and compiler verification. Marktoberdorf summer school, Germany, 2009.
- Compilation and abstract machines, part1 and part 2 (in French), École Jeunes Chercheurs en Programmation, France, 2007.
- Language-based security for mobile code, with applications to smart cards, TECS Week, Pune (India), 2005.
- Compiling functional languages, Spring school on Semantics of programming languages, Agay (France), 2002.