# Popularization talks

- 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

- 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.