Invited conference talks

• 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

• Du langage à l'action: compilation et typage (in French), tutorial lecture given at Collège de France in Gérard Berry's 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.