The Gallium project-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.
The Caml
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;
-
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
Post-doctoral openings
INRIA opened a number of post-doc positions. Applications at
the Gallium team are welcome. We are particularly interested in the following three research themes:
Advanced type systems for programming languages
Hybrid contract checking for pure functional languages
Mechanized verification of compilers
Dana N. Xu joins the Gallium team
Dana N. Xu is now an INRIA research scientist
in the Gallium team. Welcome, Dana!
Ph.D. defense of Jean-Baptiste Tristan
Jean-Baptiste Tristan successfully defended his
Ph.D. thesis,
Formal verification of translation validators,
at University Paris 7 Diderot. Congratulations, Jean-Baptiste!
A paper accepted at POPL 2010
The following paper will be presented at POPL 2010:
A simple, verified validator for software pipelining
by Jean-Baptiste Tristan and Xavier Leroy.
Ph.D. defense of Zaynah Dargaye
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!
Post-doctoral openings -- now closed
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.
A paper accepted at PLDI 2009
The following paper will be presented at PLDI 2009:
Verified validation of Lazy Code Motion
by Jean-Baptiste Tristan and Xavier Leroy.
Ph.D. defense of Boris Yakobowski
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.
Habilitation defense of Sandrine Blazy
Sandrine Blazy
successfully defended her
Habilitation à diriger les recherches at University of Évry Val d'Essone.
Congratulations, Sandrine!
Two papers accepted at POPL 2009
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.
Three papers accepted at ICFP 2008
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.
Release of Compcert
First public release of the Compcert verified C compiler.
Ph.D. defense of Yann Régis-Gianas
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!
New offices
Gallium just moved to building 14
of the Rocquencourt campus, also known as the "Miami Vice"
building (because of its pink stone facings).
Two papers accepted at POPL 2008
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.
Monpetit prize
Xavier Leroy was awarded the 2007 Michel Monpetit prize
of the French Academy of Sciences.
Three new Ph.D. students
Having brilliantly defended their MPRI master's internships,
Arthur Charguéraud,
Benoît Montagu and
Tahina Ramananandro
start their PhDs in the Gallium team.