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. The OCaml functional 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.
Nicolas Pouillard successfully defended his Ph.D. thesis, Namely, Painless: A unifying approach to safe programming with first-order syntax with binders at University Paris 7 Diderot. Congratulations, Nicolas!
Tahina Ramananandro successfully defended his Ph.D. thesis, Machine-checked Formal Semantics and Verified Compilation for C++ Objects at University Paris 7 Diderot. Congratulations, Tahina!
Xavier Leroy, Sandrine Blazy, Zaynah Dargaye and Jean-Baptiste Tristan received the 2011 award in Information Sciences of the La Recherche science monthly.
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.
The following paper will be presented at ICFP 2011: Nameless, Painless by Nicolas Pouillard.
Arthur Charguéraud successfully defended his Ph.D. thesis, Characteristic formulae for mechanized program verification at University Paris 7 Diderot. Congratulations, Arthur!
Benoît Montagu successfully defended his Ph.D. thesis, Programming with first-class modules in a core language with subtyping, singleton kinds and open existential types at École Polytechnique. Congratulations, Benoît!
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.
OCaml 3.12.0 is released. It includes a number of long-awaited new features, including first-class modules, polymorphic recursion, and much more.
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.
Dana N. Xu is now an INRIA research scientist in the Gallium team. Welcome, Dana!
Jean-Baptiste Tristan successfully defended his Ph.D. thesis, Formal verification of translation validators, at University Paris 7 Diderot. Congratulations, Jean-Baptiste!
The following paper will be presented at POPL 2010: A simple, verified validator for software pipelining by Jean-Baptiste Tristan and Xavier Leroy.
Zaynah Dargaye successfully defended her Ph.D. thesis, Vérification formelle d'un compilateur optimisant pour langages fonctionnels at University Paris 7 Diderot. Congratulations, Zaynah!
INRIA opened a number of post-doc positions. Applications at the Gallium team are welcome! See the proposed topics and contact us for more information. Updated 2009-06-30: these positions are now closed.
The following paper will be presented at PLDI 2009: Verified validation of Lazy Code Motion by Jean-Baptiste Tristan and Xavier Leroy.
Boris Yakobowski successfully defended his Ph.D. thesis, Types et contraintes graphiques : polymorphisme de second ordre et inférence, at University Paris 7 Diderot. Congratulations to Boris.
Sandrine Blazy successfully defended her Habilitation à diriger les recherches at University of Évry Val d'Essone. Congratulations, Sandrine!
The following papers will be presented at POPL 2009: Modeling Abstract Types in Modules with Open Existential Types by Benoît Montagu and Didier Rémy; A Foundation for Flow-Based Program Matching Using Temporal Logic and Model Checking by Julien Brunel, Damien Doligez, René Rydhof Hansen, Julia L. Lawall and Gilles Muller.
The following papers will be presented at ICFP 2008: Functional Translation of a Calculus of Capabilities by Arthur Charguéraud and François Pottier; Graphic Type Constraints and Efficient Type Inference: from ML to MLF, by Boris Yakobowski and Didier Rémy; and Quotient Lenses, by J. Nathan Foster, Alexandre Pilkiewicz and Benjamin C. Pierce.
Yann Régis-Gianas successfully defended his Ph.D. thesis, From types to logical assertions: automated or user-assisted proof of properties of functional programs, at University Paris 7 Diderot. Congratulations, Yann!
Gallium just moved to building 14 of the Rocquencourt campus, also known as the "Miami Vice" building (because of its pink stone facings).
The following papers will be presented at POPL 2008: Engineering Formal Metatheory by B. Aydemir, A. Charguéraud, B. C. Pierce, R. Pollack and S. Weirich, and Formal verification of translation validators: A case study on instruction scheduling optimizations, by J.-B. Tristan and X. Leroy.
Xavier Leroy was awarded the 2007 Michel Monpetit prize of the French Academy of Sciences.
Having brilliantly defended their MPRI master's internships, Arthur Charguéraud, Benoît Montagu and Tahina Ramananandro start their PhDs in the Gallium team.