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 for our work on the CompCert formally-verified compiler.
[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.)