Invited conference talks
- Trust in programming tools: the formal verification of compilers and static analysers, Verified Trustworthy Software Systems, London, April 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.
- 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.
- 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.