Cambium is a joint research team between Inria and Collège de France. It is physically located at the Inria Paris research center. It was created in 2019 and is the successor to the Gallium team.
At Cambium, we conduct research on the design, formalization and implementation of programming languages and systems. The OCaml programming language and the CompCert verified compiler embody many of our research results. Our objective is to improve the reliability of software systems through:
Follow the links at the top of this page to learn more about who we are and what we do.
Timothée Huneau joins Cambium as a PhD student, advised by Yannick Forster, Dominik Kirst and Sam van Gool. Jean Caspar joins us as an intern for the next 5 months, advised by Yannick Forster. Litao Zhou joins us as an engineer for the next 6 months, and will be collaborating with Didier Rémy. Welcome!
Mathis Bouverot-Dupuis joins Cambium as a PhD student, advised by Yannick Forster and François Pottier. Welcome!
Clément Pinard (L3), Juliette Ponsonnet (L3), and Hugo Ségoufin-Chollet (L3) join Cambium as interns. Welcome!
Simon Dima (M2) and Zhicheng Hui (M1) join Cambium as interns. Welcome!
Clément Blaudeau defended his PhD thesis on December 11 and Frédéric Bour defended on December 18. Congratulations!
Nathanaëlle Courant and Alexandre Moine have defended their PhD theses on September 19 and September 20. Congratulations!
Tiago Soares and Samuel Vivien join Cambium as PhD students. Mathis Bouverot-Dupuis joins Cambium for a 6-month internship. Welcome!
The paper A Two-Phase Infinite/Finite Low-Level Memory Model by Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski, and Steve Zdancewic has been accepted for presentation at ICFP 2024.
The paper Snapshottable Stores by Clément Allain, Basile Clément, Alexandre Moine, and Gabriel Scherer, has been accepted for presentation at ICFP 2024 and has received a distinguished paper award. Congratulations!
The paper Separating Markov's Principles by Liron Cohen, Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva, and Vincent Rahli, has been accepted for presentation at LICS 2024.
The paper Verified Extraction from Coq to OCaml by Yannick Forster, Matthieu Sozeau, and Nicolas Tabareau, has been accepted for presentation at PLDI 2024, and has received a Distinguished Paper Award.
Malo Monin (L3) and Wassel Bousmaha (L3) join Cambium for six-week research internships. Welcome!
The paper Fulfilling OCaml Modules with Transparency by Clément Blaudeau, Didier Rémy and Gabriel Radanne has been accepted for presentation at OOPSLA 2024.
Weituo Dai (M2), Yee-Jian Tan (M1) and Poiraz Yilan (M1) join Cambium for research internships. Welcome!
Jules Viennot (M2) joins Cambium for a research internship. Welcome!
Irene Yoon joins our team on a 12-month postdoctoral position. Welcome, Irene!
The paper Correct tout seul, sûr à plusieurs by Clément Allain and Gabriel Scherer and the paper Correct, fast LR(1) unparsing by François Pottier have been accepted for presentation at JFLA 2024.
Yannick Forster joins our team on a permanent position as a chargé de recherche (junior researcher). Welcome, Yannick!
OCaml receives the prix science ouverte du logiciel libre de la recherche 2023, a prize awarded by the French Ministry for Higher Education and Research. It is one among eight distinguished free software projects across all scientific disciplines.
Remy Seassau, advised by François Pottier, and Tiago Soares, advised by Mário Pereira and François Pottier, join the team as PhD students. Welcome!
The paper Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library by Paulo Emílio de Vilhena and François Pottier has been accepted for publication in Logical Methods in Computer Science.
OCaml receives ACM SIGPLAN's Programming Languages Software Award for the year 2023. Congratulations to all contributors and in particular to Xavier Leroy, Luc Maranget, Florian Angeletti, and Damien Doligez, who are members of the Cambium team, for this award.
Xavier Leroy becomes a member of Académie des Sciences. Congratulations!
Paulo Emílio de Vilhena receives the 2023 GDR GPL Award for his dissertation entitled Proof of Programs with Effect Handlers. Congratulations!
Arnaud Daby-Seesaram (M2) joins Cambium for a research internship during the coming spring. Welcome!
The paper A Type System for Effect Handlers and Dynamic Labels by Paulo Emílio de Vilhena and François Pottier has been accepted for presentation at ESOP 2023.
Glen Mével and Paulo Emílio de Vilhena have defended their PhD thesis. Congratulations!
The paper A high-level separation logic for heap space under garbage collection by Alexandre Moine, Arthur Charguéraud and François Pottier has been accepted for presentation at POPL 2023.
The paper A conceptual framework for safe object initialization: a principled and mechanized soundness proof of the Celsius model by Clément Blaudeau and Fengyun Liu has been accepted for presentation at OOPSLA 2022.
Xavier Leroy receives the 2022 ACM SIGPLAN Programming Languages Achievement Award for his work on OCaml and CompCert. "Both of these projects have had enormous impact in the PL community and beyond, and they have significantly pushed the boundaries of what is perceived as possible," the citation acknowledges. Congratulations!
The CompCert verified compiler, whose authors include team member Xavier Leroy and former team members Sandrine Blazy, Zaynah Dargaye, Jacques-Henri Jourdan and Jean-Baptiste Tristan, has received the 2021 ACM Software System Award.
Clément Allain (M2) and Guillaume Bertholon (M2) join Cambium for research internships during the coming spring. Welcome!
The paper End-to-End Translation Validation for the Halide Language by Basile Clément and Albert Cohen, has been accepted for presentation at OOPSLA 2022.
Cambium alumnus Armaël Guéneau joins Inria Saclay as a researcher. Congratulations!
The paper Specification and Verification of a Transient Stack by Alexandre Moine, Arthur Charguéraud and François Pottier has been accepted for presentation at CPP 2022, and has received a Distinguished Paper Award.
The papers A Separation Logic for Heap Space under Garbage Collection by Jean-Marie Madiot and François Pottier and Extending Intel-x86 Consistency and Persistency by Azalea Raad, Luc Maranget and Viktor Vafeiadis have been accepted for presentation at POPL 2022.
Clément Blaudeau and Alexandre Moine join Cambium as PhD students. Welcome!
The paper Faster Reachability Analysis for LR(1) Parsers by Frédéric Bour and François Pottier has been accepted for presentation at SLE 2021.
The paper Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model by Glen Mével and Jacques-Henri Jourdan has been accepted for presentation at ICFP 2021.
Clément Blaudeau (M2), Alexandre Moine (M2) and Émile Trotignon (M1) have joined Cambium for research internships during the coming spring. Welcome!
Ambre Williams defended her PhD on Refactoring functional programs with ornaments. Congratulations!
The papers Mécanisation du modèle RC11 et de la propriété DRF-SC by Quentin Ladeveze and Strong automated testing of OCaml libraries by François Pottier have been accepted for presentation at JFLA 2021.
Gabriel Radanne leaves our group to take a permanent position as an Inria researcher in the CASH research team in Lyons. Congratulations!
The papers Verified Code Generation for the Polyhedral Model by Nathanaël Courant and Xavier Leroy and A separation logic for effect handlers by Paulo Emílio de Vilhena and François Pottier have been accepted for presentation at POPL 2021.
The paper Provably and practically efficient granularity control by our former colleagues Umut Acar, Vitaly Aksenov, Arthur Charguéraud, and Mike Rainey has been recognized as a SIGPLAN Research Highlight. Congratulations!
The papers Kindly Bent to Free Us by Gabriel Radanne, Hannes Saffrich, and Peter Thiemann and Cosmo: A concurrent separation logic for Multicore OCaml by Glen Mével, Jacques-Henri Jourdan, and François Pottier have been accepted for presentation at ICFP 2020.
The paper Algebraically Closed Fields in Isabelle/HOL by Paulo Emílio de Vilhena and Lawrence Paulson has been accepted for presentation at IJCAR 2020.
The paper ARMv8-A system semantics: instruction fetch in relaxed architectures by Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, and Peter Sewell has been accepted for presentation at ESOP 2020.
Thomas Refis joins our team as a Ph.D. student. Welcome!
Our student Armaël Guéneau has defended his thesis on Monday, December 16, 2019.
The paper Spy game: Verifying a local generic solver in Iris by Paulo Emílio de Vilhena, François Pottier, and Jacques-Henri Jourdan has been accepted for presentation at POPL 2020.
Quite a few people have joined us between September and November 2019. Frédéric Bour, Basile Clément, Nathanaël Courant, Quentin Ladeveze, and Paulo Emílio de Vilhena have joined the team as Ph.D. students. Jacques Garrigue will be visiting us until June 2020. Gabriel Radanne has been recruited on a 3-year starting research position, and Florian Angeletti has been recruited as an engineer, also for a 3-year term. Welcome!