Fabrice Le Fessant and Luc Maranget join the Gallium team
- 2013-01-02
The Gallium team welcomes Fabrice Le Fessant and Luc Maranget, INRIA research scientists.
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. 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:
- 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
Verified Software Milestone Award
- 2012-12-19
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
- 2012-10-15
Thibaut Balabonski just started a post-doc in the Gallium team. Welcome, Thibaut!
Thomas Braibant joins the Gallium team
- 2012-09-03
Thomas Braibant just started a post-doc in the Gallium team. Welcome, Thomas!
OCaml 4.00 released
- 2012-07-26
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 external tools.
The Gagallium blog
- 2012-07-09
Some of our members now chronicle their thoughts on the Gagallium blog. Happy reading!
Ph.D. defense of Nicolas Pouillard
- 2012-01-13
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!
Ph.D. defense of Tahina Ramananandro
- 2012-01-10
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!
La Recherche award in Information Sciences
- 2011-10-18
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
- 2011-10-06
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
- 2011-06-01
The following paper will be presented at ICFP 2011: Nameless, Painless by Nicolas Pouillard.
Ph.D. defense of Arthur Charguéraud
- 2010-12-16
Arthur Charguéraud successfully defended his Ph.D. thesis, Characteristic formulae for mechanized program verification at University Paris 7 Diderot. Congratulations, Arthur!
Ph.D. defense of Benoît Montagu
- 2010-12-15
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!
Two papers accepted at POPL 2011
- 2010-10-04
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
- 2010-08-02
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
- 2010-06-08
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.