Hello and welcome to my corner of the Web. I'm a senior computer scientist interested in all scientific aspects of computer programming. I'm a professor at Collège de France, where I hold the chair of software sciences, and a member of Académie des sciences. I'm also a member of the Cambium research team of Inria.
News
[05/2023] Lecture material: slides in English are now available for my Collège de France lectures on Persistent data structures.
[03/2023] Award: I am honored to receive the 2023 Lucas Award from Formal Methods Europe, along with Sandrine Blazy and Zaynah Dargaye, for a highly influential paper published at the FM 2006 conference.
[02/2023] Lecture material (in French): Théorie et pratique des effets en OCaml 5, JFLA 2023.
[01/2023] Publication: Efficient extensional binary tries, with Andrew Appel, in Journal of Automated Reasoning.
[01/2023] Award: I am honored to receive the 2022 ACM SIGPLAN Programming Languages Software Award along with my co-workers Sandrine Blazy, Zaynah Dargaye, Jacques-Henri Jourdan, Michael Schmidt, Bernhard Schommer, and Jean-Baptiste Tristan.
[12/2022] Appointment: I have been elected a member of the Académie des sciences of Institut de France.
[12/2022] Software: OCaml 5.0 was released! It features two major extensions of the OCaml programming language, namely shared-memory concurrency and effects with effect handlers, and required many years of work by the OCaml and Multicore OCaml development teams.
[10/2022] Lecture material: slides in English are now available for my Collège de France lectures on Language-based software security.
[09/2022] Award: I am deeply honored to receive the 2022 ACM SIGPLAN Programming Languages Achievement Award for "fundamental contributions to both the theory and practice of programming languages on a range of topics, including type system and module system design, efficient compilation of functional programming languages, bytecode verification, verified compilation, and verified static analysis".
[05/2022] Award: I am deeply honored to receive the 2021 ACM Software System Award for my work on the CompCert formally-verified compiler, along with my co-workers Sandrine Blazy, Zaynah Dargaye, Jacques-Henri Jourdan, Michael Schmidt, Bernhard Schommer, and Jean-Baptiste Tristan.
[07/2021] Lecture material: slides in English are now available for my Collège de France lectures on Program logics.
[11/2020] Publication: Verified Code Generation for the Polyhedral Model, by Nathanaël Courant and I, to be presented at POPL 2021, with accompanying Coq development.
[10/2020] Lecture material: slides in English are now available for my Collège de France lectures on The Curry-howard correspondence today (2018-2019) and on Mechanized semantics (2019-2020). See also the companion Coq development.
[12/2019] Publication: the text of my inaugural lecture at Collège de France, Software, between mind and matter, is now available freely: in the original French at OpenEdition Books (HTML) and at HAL (PDF); and in English through a preliminary translation (PDF and e-book).
[04/2019] Publication (in French): the text of my inaugural lecture at Collège de France, Le logiciel, entre l'esprit et la matière, is now available as a book and an e-book. The video of the lecture is still available, in the original French.
[11/2018] Appointment: I am proud to be appointed professor at Collège de France on the chair of software sciences. It's a great honor but also a great responsibility! (This is the second permanent chair in computer science at Collège de France, after Gérard Berry's chair.)
[07/2018] Award: I am honored to receive the Grand prix Inria - Académie des sciences 2018.
[01/2018] Publication: CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler, by Daniel Kästner et al, presented at ERTS 2018. This paper describes the first use of CompCert in production for a safety-critical application in the nuclear industry, including IEC 60880 certification.
[12/2017] I was interviewed by Jean Yang as part of a "People of Programming Languages" series.
[06/2017] Publication: A Formally Verified Compiler for Lustre, by Timothy Bourke, Lélio Brun, Pierre-Evariste Dagand, myself, Marc Pouzet and Lionel Rieg, PLDI 2017.
[02/2017] Software and Coq development: version 3.0 of Compcert is released. This is the first CompCert version that fully supports 64-bit target processors; more precisely, pointers and memory addresses are no longer assumed to be 32-bit wide and can be 64-bit wide as well depending on the target. Definitely 3.0 material!
[11/2016] Public lecture: video of my Milner award lecture at the Royal Society.
[11/2016] Award: I am deeply honored to receive one of the two 2016 van Wijngaarden awards from CWI.
[01/2016] Award: my POPL 2006 paper, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, received the ACM SIGPLAN Most Influential POPL Paper Award.