The Cambium research team

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:

  • higher-level, safer, more expressive programming languages based on the 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 mechanized proofs of programs.

Follow the links at the top of this page to learn more about who we are and what we do.


Two papers at POPL 2022

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.

Léo Stefanesco defends

Léo Stefanesco has defended his PhD thesis. Congratulations!

New PhD students at Cambium

Clément Blaudeau and Alexandre Moine join Cambium as PhD students. Welcome!

A paper at SLE 2021

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.

A paper at ICFP 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.

New interns at Cambium

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

Ambre Williams defended her PhD on Refactoring functional programs with ornaments. Congratulations!

Two papers at JFLA 2021

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 Cambium

Gabriel Radanne leaves our group to take a permanent position as an Inria researcher in the CASH research team in Lyons. Congratulations!

Two papers at POPL 2021

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.

Léo Stefanesco joins Cambium

Léo Stefanesco joins our team for the coming year. Welcome!

A research highlight

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!

Two papers at ICFP 2020

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.

A paper at IJCAR 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.

A paper at ESOP 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.

New members

Thomas Refis joins our team as a Ph.D. student. Welcome!

Armaël Guéneau defends

Our student Armaël Guéneau has defended his thesis on Monday, December 16, 2019.

A paper at POPL 2020

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.

New members

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!