The Cambium research team
Cambium is a joint research team betweenInria andCollège de France. It is physically located at theInria Paris research center. It was created in 2019 and is the successor to theGallium team.
At Cambium, we conduct research on the design, formalization andimplementation of programming languages and systems.TheOCaml programming language andtheCompCert verified compilerembody many of our research results. Our objective is toimprove the reliability of software systems through:
- higher-level, safer, more expressive programming languages based onthe functional programming paradigm;
- automatic error detection via type systems and related static analyses;
- high-assurance code generation tools and program verification tools;
- better linguistic support for formal methods, especially mechanizedproofs of programs.
Follow the links at the top of this page to learn more aboutwho we are and what we do.
News
New interns at Cambium
- 2025-03-24
Simon Dima (M2) and Zhicheng Hui (M1) join Cambium as interns. Welcome!
PhD defenses
- 2024-12-18
Clément Blaudeau defended his PhD thesis on December 11 andFrédéric Bour defended on December 18. Congratulations!
PhD defenses
- 2024-09-20
Nathanaëlle Courant andAlexandre Moine have defended their PhD theses on September 19 and September 20. Congratulations!
New students at Cambium
- 2024-09-09
Tiago Soares and Samuel Vivien join Cambium as PhD students. Mathis Bouverot-Dupuis joins Cambium for a 6-month internship. Welcome!
A paper at ICFP 2024
- 2024-09-09
The paperA 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.
A (distinguished!) paper at ICFP 2024
- 2024-08-27
The paperSnapshottable Stores by Clément Allain,Basile Clément,Alexandre Moine, and Gabriel Scherer, has been accepted for presentation at ICFP 2024 and has received adistinguished paper award. Congratulations!
A paper at LICS 2024
- 2024-06-21
The paperSeparating 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.
A paper at PLDI 2024
- 2024-06-21
The paperVerified Extraction from Coq to OCaml byYannick Forster, Matthieu Sozeau, and Nicolas Tabareau, has been accepted for presentation at PLDI 2024, and has received aDistinguished Paper Award.
New interns at Cambium
- 2024-05-27
Malo Monin (L3) and Wassel Bousmaha (L3) join Cambium for six-week research internships. Welcome!
A paper at OOPSLA 2024
- 2024-05-27
The paperFulfilling OCaml Modules with Transparency byClément Blaudeau,Didier Rémy and Gabriel Radanne has been accepted for presentation at OOPSLA 2024.
New interns at Cambium
- 2024-05-02
Weituo Dai (M2), Yee-Jian Tan (M1) and Poiraz Yilan (M1) join Cambium for research internships. Welcome!
A new intern at Cambium
- 2024-04-02
Jules Viennot (M2) joins Cambium for a research internship. Welcome!
Cambium welcomes Irene Yoon
- 2024-02-01
Irene Yoon joins our team on a 12-month postdoctoral position. Welcome, Irene!
Two papers at JFLA 2024
- 2024-01-25
The paperCorrect tout seul, sûr à plusieurs by Clément Allain andGabriel Scherer and the paperCorrect, fast LR(1) unparsing byFrançois Pottier have been accepted for presentation atJFLA 2024.
Cambium welcomes Yannick Forster
- 2023-12-01
Yannick Forster joins our team on a permanent position as achargé de recherche (junior researcher). Welcome, Yannick!
OCaml receives Open Science Prize for Free Software
- 2023-11-29
OCaml receives theprix 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.
New students at Cambium
- 2023-10-01
Remy Seassau, advised by François Pottier, and Tiago Soares, advised byMário Pereira and François Pottier, join the team as PhD students. Welcome!
A paper in LMCS
- 2023-07-28
The paperVerifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library byPaulo Emílio de Vilhena andFrançois Pottier has been accepted for publication inLogical Methods in Computer Science.
OCaml receives Programming Languages Software Award
- 2023-06-20
OCaml receives ACM SIGPLAN'sProgramming Languages Software Award for the year 2023. Congratulations to all contributors and in particular toXavier Leroy,Luc Maranget,Florian Angeletti, andDamien Doligez, who are members of the Cambium team, for this award.
Xavier Leroy elected at Académie des Sciences
- 2023-06-06
Xavier Leroy becomes a member ofAcadémie des Sciences. Congratulations!
Paulo de Vilhena receives GDR GPL Dissertation Award
- 2023-06-06
Paulo Emílio de Vilhena receives the2023 GDR GPL Award for his dissertation entitledProof of Programs with Effect Handlers. Congratulations!
A new intern at Cambium
- 2023-03-14
Arnaud Daby-Seesaram (M2) joins Cambium for a research internship during the coming spring. Welcome!
A paper at ESOP 2023
- 2023-01-27
The paperA Type System for Effect Handlers and Dynamic Labels byPaulo Emílio de Vilhena andFrançois Pottier has been accepted for presentation at ESOP 2023.
Glen Mével and Paulo de Vilhena defend
- 2022-12-16
Glen Mével andPaulo Emílio de Vilhena have defended their PhD thesis. Congratulations!
A paper at POPL 2023
- 2022-11-25
The paperA high-level separation logic for heap space under garbage collection byAlexandre Moine, Arthur Charguéraud andFrançois Pottier has been accepted for presentation at POPL 2023.
A paper at OOPSLA 2022
- 2022-11-25
The paperA conceptual framework for safe object initialization: a principled and mechanized soundness proof of the Celsius model byClément Blaudeau and Fengyun Liu has been accepted for presentation at OOPSLA 2022.
Xavier Leroy receives ACM SIGPLAN Programming Languages Achievement Award
- 2022-09-14
Xavier Leroy receives the 2022ACM 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!
CompCert receives ACM Software System Award
- 2022-05-11
TheCompCert verified compiler, whose authors include team memberXavier Leroy and former team members Sandrine Blazy, Zaynah Dargaye, Jacques-Henri Jourdan and Jean-Baptiste Tristan, has receivedthe 2021 ACM Software System Award.
New interns at Cambium
- 2022-03-18
Clément Allain (M2) and Guillaume Bertholon (M2) join Cambium for research internships during the coming spring. Welcome!
A paper at OOPSLA 2022
- 2022-03-09
The paperEnd-to-End Translation Validation for the Halide Language byBasile Clément and Albert Cohen, has been accepted for presentation at OOPSLA 2022.
Armaël Guéneau joins Inria
- 2022-01-01
Cambium alumnusArmaël Guéneau joins Inria Saclay as a researcher. Congratulations!
A paper at CPP 2022
- 2021-12-09
The paperSpecification and Verification of a Transient Stack byAlexandre Moine,Arthur Charguéraud andFrançois Pottier has been accepted for presentation at CPP 2022, and has received a Distinguished Paper Award.
Two papers at POPL 2022
- 2021-11-14
The papersA Separation Logic for Heap Space under Garbage Collection byJean-Marie Madiot andFrançois Pottier andExtending Intel-x86 Consistency and Persistency by Azalea Raad,Luc Maranget and Viktor Vafeiadis have been accepted for presentation at POPL 2022.
New PhD students at Cambium
- 2021-10-01
Clément Blaudeau andAlexandre Moine join Cambium as PhD students. Welcome!
A paper at SLE 2021
- 2021-09-27
The paperFaster Reachability Analysis for LR(1) Parsers byFrédéric Bour andFrançois Pottier has been accepted for presentation at SLE 2021.
A paper at ICFP 2021
- 2021-07-06
The paperFormal Verification of a Concurrent Bounded Queue in a Weak Memory Model byGlen Mével and Jacques-Henri Jourdan has been accepted for presentation at ICFP 2021.
New interns at Cambium
- 2021-03-18
Clément Blaudeau (M2), Alexandre Moine (M2) and Émile Trotignon (M1) have joined Cambium for research internships during the coming spring. Welcome!
Ambre Williams graduates
- 2020-12-14
Ambre Williams defended her PhD on Refactoring functional programs with ornaments. Congratulations!
Two papers at JFLA 2021
- 2020-12-12
The papersMécanisation du modèle RC11 et de la propriété DRF-SC byQuentin Ladeveze andStrong automated testing of OCaml libraries byFrançois Pottier have been accepted for presentation atJFLA 2021.
Gabriel Radanne leaves Cambium
- 2020-12-01
Gabriel Radanne leaves our group to take a permanent position as an Inria researcher in theCASH research team in Lyons. Congratulations!
Two papers at POPL 2021
- 2020-11-07
The papersVerified Code Generation for the Polyhedral Model byNathanaël Courant andXavier Leroy andA separation logic for effect handlers byPaulo Emílio de Vilhena andFrançois Pottier have been accepted for presentation atPOPL 2021.
A research highlight
- 2020-08-05
The paperProvably and practically efficient granularity control by our former colleagues Umut Acar, Vitaly Aksenov, Arthur Charguéraud, and Mike Rainey has been recognized as aSIGPLAN Research Highlight. Congratulations!
Two papers at ICFP 2020
- 2020-06-12
The papersKindly Bent to Free Us byGabriel Radanne, Hannes Saffrich, and Peter Thiemann andCosmo: A concurrent separation logic for Multicore OCaml byGlen Mével, Jacques-Henri Jourdan, andFrançois Pottier have been accepted for presentation at ICFP 2020.
A paper at IJCAR 2020
- 2020-03-30
The paperAlgebraically Closed Fields in Isabelle/HOL byPaulo Emílio de Vilhena and Lawrence Paulson has been accepted for presentation at IJCAR 2020.
A paper at ESOP 2020
- 2020-03-17
The paperARMv8-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.
New members
- 2020-02-04
Thomas Refis joins our team as a Ph.D. student. Welcome!
Armaël Guéneau defends
- 2019-12-16
Our studentArmaël Guéneau has defended his thesis on Monday, December 16, 2019.
A paper at POPL 2020
- 2019-11-20
The paperSpy game: Verifying a local generic solver in Iris byPaulo Emílio de Vilhena,François Pottier, and Jacques-Henri Jourdan has been accepted for presentation at POPL 2020.
New members
- 2019-11-20
Quite a few people have joined us between September and November 2019.Frédéric Bour, Basile Clément,Nathanaël Courant,Quentin Ladeveze, andPaulo 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!