ACM Fellow
- 2015-12-09
Xavier Leroy was appointed Fellow of the ACM "for contributions to safe, high-performance functional programming languages and compilers, and to compiler verification".
News archive
Royal Society Milner award
- 2015-07-20
Xavier Leroy was awarded the 2016 Royal Society Milner Award "in recognition of his exceptional achievements in computer programming which includes the design and implementation of the OCaml programming language".
A paper accepted at ICFP 2015
- 2015-06-04
The following paper will be presented at ICFP 2015: Which simple types have a unique inhabitant?, by Gabriel Scherer and Didier Rémy.
First release of the Verasco verified static analyzer
- 2014-10-28
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
- 2014-10-28
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
- 2014-10-01
Maxime Dénès joins the Gallium team as a post-doctoral fellow. Welcome, Maxime!
Ph.D. defense of Jonathan Protzenko
- 2014-09-29
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
- 2014-09-03
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
- 2014-08-29
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
- 2014-06-04
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
- 2014-03-31
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
- 2014-01-30
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
- 2013-11-04
Pierre-Évariste Dagand is now a post-doctoral fellow in the Gallium team. Welcome, Pierre!
Most Influential ICFP Paper Award
- 2013-09-27
Didier Le Botlan and Didier Rémy received the ACM SIGPLAN Most Influential ICFP Paper Award for their ICFP 2003 paper, MLF: Raising ML to the power of System F.
OCaml 4.01 released
- 2013-09-12
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
- 2013-06-21
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
- 2013-06-14
The following papers will be presented at ICFP 2013: Programming with Permissions in Mezzo by François Pottier and Jonathan Protzenko, and 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
- 2013-06-03
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
- 2013-01-02
The Gallium team welcomes Fabrice Le Fessant and Luc Maranget, INRIA research scientists.
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.