The Cambium research team

Cambium is an Inria team, part of the 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.

News

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 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!