The Gallium research team
Gallium is a project-team of INRIA,
part of the Paris-Rocquencourt
research center, located in the western suburbs of Paris.
Created in January 2006, it is the successor to the Cristal team.
At Gallium, we conduct research on the design, formalization and
implementation of programming languages and systems.
functional 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.
First release of the Verasco verified static analyzer
The Verasco static analyzer verifies the absence of run-time errors in C programs using static analysis techniques based on abstract interpretation. The novelty of Verasco is that it is entirely specified and proved sound using the Coq proof assistant. The first public release is available here. The paper below gives more details on the design and verification of Verasco.
A paper accepted at POPL 2015
The following paper will be presented at POPL 2015:
A formally-verified C static analyzer,
by Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie.
Maxime Dénès joins the Gallium team
Maxime Dénès joins the
Gallium team as a post-doctoral fellow. Welcome, Maxime!
Ph.D. defense of Jonathan Protzenko
Jonathan Protzenko successfully defended his Ph.D. thesis,
Mezzo, a typed language for safe effectful concurrent programs
at University Paris Diderot. Congratulations, Jonathan!
ICFP 2014 programming contest, Judge's prize
Team gagallium (François Bobot, Pierre Boutillier, Thomas Braibant, Damien Doligez, and Gabriel Scherer) were awarded the Judge's prize at the ICFP 2014 programming contest. In the words of the judge, Team gagallium are an extremely cool bunch of hackers!
OCaml 4.02 released
OCaml version 4.02.0 is now available. This major release adds many long-awaited language features and brings some performance improvements. Enjoy!
A paper accepted at ICFP 2014
The following paper will be presented at ICFP 2014:
Hindley-Milner elaboration in applicative style
by François Pottier.
A paper accepted at CSL-LICS 2014
The following paper will be presented at CSL-LICS 2014:
System F with Coercion Constraints
by Julien Cretin and Didier Rémy.
Ph.D. defense of Julien Cretin
Julien Cretin successfully defended his Ph.D. thesis,
Erasable coercions: a unified approach to type systems
at University Paris Diderot. Congratulations, Julien!
Pierre-Évariste Dagand joins the Gallium team
Pierre-Évariste Dagand is now a post-doctoral fellow in the Gallium team. Welcome, Pierre!
OCaml 4.01 released
Version 4.01 of the OCaml system is now available. This is a major release that introduces type-based disambiguation of constructors and record field labels and a whole lot of new warnings, among other new features.
CompCert 2.0 released
The Compcert C verified compiler
reaches the 2.0 landmark with full support for 64-bit integers and a new register allocator based on end-to-end translation validation.
Two papers accepted at ICFP 2013
The following papers will be presented at ICFP 2013:
Programming with Permissions in Mezzo
by François Pottier and Jonathan Protzenko,
Weak Optimality, and the Meaning of Sharing
by Thibaut Balabonski.
Umut Acar and Mike Rainey join the Gallium team to start the ERC DeepSea project
Umut Acar, assistant professor at CMU, and Mike Rainey join the Gallium team on, respectively, a part-time Inria advanced research position and an Inria starting research position. They will work on the DeepSea project, funded by the European Research Council, whose goal is to develop novel approaches to dynamic parallelism. Welcome, Umut and Mike!
Fabrice Le Fessant and Luc Maranget join the Gallium team
The Gallium team welcomes Fabrice Le Fessant and Luc Maranget, INRIA research scientists.
Verified Software Milestone Award
Xavier Leroy was awarded the
Microsoft Research Verified Software Milestone Award in recognition of his work on the CompCert formally-verified compiler.
Thibaut Balabonski joins the Gallium team
Thibaut Balabonski just started a post-doc in the Gallium team. Welcome, Thibaut!
Thomas Braibant joins the Gallium team
Thomas Braibant just started a post-doc in the Gallium team. Welcome, Thomas!
OCaml 4.00 released
Version 4.00 of the OCaml system is now available. Novelties include
generalized algebraic datatypes (GADTs), improved support for
first-class modules, and a "bin-annot" mechanism
to communicate typed abstract syntax trees to IDEs and similar
The Gagallium blog
Some of our members now chronicle their thoughts on the
Ph.D. defense of Nicolas Pouillard
Nicolas Pouillard successfully defended his
Namely, Painless: A unifying approach to safe programming
with first-order syntax with binders
at University Paris 7 Diderot. Congratulations, Nicolas!
Ph.D. defense of Tahina Ramananandro
Tahina Ramananandro successfully defended his
Machine-checked Formal Semantics and Verified Compilation for C++ Objects
at University Paris 7 Diderot. Congratulations, Tahina!
La Recherche award in Information Sciences
Xavier Leroy, Sandrine Blazy, Zaynah Dargaye and Jean-Baptiste Tristan
received the 2011 award in Information Sciences of the La Recherche science monthly.
Two papers accepted at POPL 2012
The following papers will be presented at POPL 2012:
Extending System F-eta with Abstraction over Erasable Coercions
by Julien Cretin and Didier Rémy;
A mechanized semantics for C++ object construction and destruction, with applications to resource management by Tahina Ramananandro, Gabriel Dos Reis, and Xavier Leroy.
A paper accepted at ICFP 2011
The following paper will be presented at ICFP 2011:
Nameless, Painless by Nicolas Pouillard.
Ph.D. defense of Arthur Charguéraud
Arthur Charguéraud successfully defended his
Characteristic formulae for mechanized program verification
at University Paris 7 Diderot. Congratulations, Arthur!
Two papers accepted at POPL 2011
The following papers will be presented at POPL 2011:
A typed store-passing translation for general references
by François Pottier;
Formal verification of object layout for C++ multiple inheritance
by Tahina Ramananandro, Gabriel Dos Reis, and Xavier Leroy.
Release of OCaml 3.12.0
OCaml 3.12.0 is released. It includes a number of long-awaited new features, including first-class modules, polymorphic recursion, and much more.
Three papers accepted at ICFP 2010
The following papers will be presented at ICFP 2010:
Program Verification Through Characteristic Formulae
by Arthur Charguéraud;
A fresh look at programming with names and binders
by Nicolas Pouillard and François Pottier;
Matching Lenses: Alignment and View Update
by Davi M. J. Barbosa, Julien Cretin, Nate Foster, Michael Greenberg
and Benjamin C. Pierce.