Popularization talks

• De la logique avant toute chose! Du programme de Hilbert à la naissance de la science informatique (in French), colloquium Sciences et Société, Nancy, April 2024.
• Quelle confiance en les résultats d'une IA? Erreurs, biais, et autres risques (in French), short presentation for the Campus de l'innovation pour les lycées, Collège de France, Paris, Sept 2023.
• In search of software perfection, Milner award lecture, Royal Society, London, Nov 2016. Video of the talk.
• On programming languages and their trustworthy implementation, Van Wijngaarden award ceremony, Amsterdam, Nov 2016.
• Desperately seeking software perfection, colloquium d'informatique de l'UPMC Sorbonne Universités, Paris, Oct 2015.
• Proof assistants in computer science research, IHP thematic trimester on Semantics of proofs and certified mathematics, April 2014. Video of the talk.
• Du langage à l'action: compilation et typage (in French), tutorial lecture given at Collège de France in Gérard Berry's 2007 course. A video of the lecture is available.

Invited conference talks

• Mechanizing Abstract Interpretation, extended version of a talk given at the 2024 Next 40 years of Abstract Interpretation workshop.
• 25 years of OCaml, invited talk given at the OCaml workshop 2021. Here is a video of the talk.
• Formal verification of a code generator for a modeling language: the Velus project, invited talk given at the MARS/VPT workshop of ETAPS 2018.
• Trust in compilers, code generators, and software verification tools, invited talk given at ERTS 2018.
• Formally verifying a compiler: what does it mean, exactly?, invited talk given at ICALP 2016.
• Formal verification of a static analyzer: abstract interpretation in type theory, the 2014 Types Meeting, May 2014.
• Mechanized semantics for compiler verification, invited talk given at APLAS and CPP 2012. Extended abstract.
• Verified squared: does critical software deserve verified tools?, invited talk given at POPL 2011. Extended abstract.
• A formally verified compiler for critical embedded software, invited talk given at the LCTES conference, 2008.
• Formal verification of an optimizing compiler, invited talk given at the RTA conference, 2007.
• From Krivine's machine to the Caml implementations, invited talk given at the KAZAM workshop, 2005.
• Exploiting type systems and static analyses for smart card security, invited talk given at CASSIS'04.
• Smart card security from a programming language and static analysis perspective, invited talk given at ETAPS'03.
• Java byte code verification: an overview, invited talk given at CAV'01.
• Objects and classes versus modules in Objective Caml, invited talk given at ICFP'99.

Tutorials

• Compilation techniques for functional and object-oriented languages, tutorial given at PLDI'98, with accompanying references.
• An introduction to compiling functional languages, tutorial given at the Workshop Types in Compilation 98, with accompanying references.

See also: my lecture notes.