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
[04/2024] Lecture material: slides in English are now available for my Collège de France lectures on Control structures: from "goto" to algebraic effects.
[01/2024] Award: the 2023 ACM SIGPLAN Programming Languages Software Award was awarded to the OCaml language and system. After more than 30 years of work on Caml, it was a pleasure and an honor to stand on the scene at POPL 2024 with several other core OCaml developers to receive this award.
[01/2024] Presentation: my Coq programming pearl on Well-founded recursion done right was presented at the CoqPL 2024 workshop.
[11/2023] Award: the OCaml language and system was awarded one of the 2023 prix science ouverte du logiciel libre (open science award for free software) from the French ministry of higher education and research.
[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.)