The Gallium research team

The Gallium team has been replaced in 2019 with Cambium.

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

Armaël Guéneau defends

Our student Armaël Guéneau has defended his thesis on Monday, December 16, 2019.

A paper at POPL 2020

The paper Spy game: Verifying a local generic solver in Iris by Paulo Emílio de Vilhena, François Pottier, and Jacques-Henri Jourdan has been accepted for presentation at POPL 2020.

New members

Quite a few people have joined us between September and November 2019. Frédéric Bour, Basile Clément, Nathanaël Courant, Quentin Ladeveze, and Paulo de Vilhena have joined the team as Ph.D. students. Jacques Garrigue will be visiting us until June 2020. Gabriel Radanne has been recruited on a 3-year starting research position, and Florian Angeletti has been recruited as an engineer, also for a 3-year term. Welcome!

A paper at ESOP 2019

The following paper was presented at ESOP 2019: Time Credits and Time Receipts in Iris, by Glen Mével, Jacques-Henri Jourdan, and François Pottier.

Publication of Xavier Leroy's inaugural lecture

Xavier Leroy's inaugural lecture at Collège de France, Le logiciel, entre l’esprit et la matière, is now available online, in the original French and as a preliminary English translation.

Ph.D. defense of Vitaly Aksenov

Vitaly Aksenov successfully defended his Ph.D. thesis, Synchronization Costs in Parallel Programs and Concurrent Data Structures at ITMO University and Université Paris-Diderot. Congratulations, Vitaly!

Best paper award for Gergö Barany

The paper Finding Missed Compiler Optimizations by Differential Testing, by Gergö Barany, received the best paper award at the Compiler Construction 2018 conference.

A paper at PLDI 2018

The following paper was accepted to PLDI 2018: Heartbeat Scheduling: Provable Efficiency for Nested Parallelism by Umut Acar, Arthur Charguéraud, Adrien Guatto, Mike Rainey, Filip Sieczkowski.

A paper at POPL 2018

The following paper will be presented at POPL in January 2018: A Principled approach to Ornamentation in ML by Thomas Williams and Didier Rémy.

A paper at ICFP 2017

The following paper will be presented at ICFP in Sept 2017: Visitors Unchained by François Pottier.

GDR GPL PhD award for Jacques-Henri Jourdan

Jacques-Henri Jourdan receives the 2016 award from GDR Génie de la Programmation et du Logiciel for his PhD thesis, Verasco: a Formally Verified C Static Analyzer.

Two papers at PLDI 2017

The following two papers will be presented at PLDI in June 2017: Responsive Parallel Computation: Bridging Competitive and Cooperative Threading by Stefan K. Muller, Umut A. Acar, Robert Harper; A formally verified compiler for Lustre by Timothy Bourke, Lélio Brun, Pierre Évariste Dagand, Xavier Leroy, Marc Pouzet, and Lionel Rieg.

Gergö Barany joins the Gallium team

Gergö Barany joins Gallium on a post-doc position. Welcome, Gergö!

CompCert 3.0 released, with full 64-bit support

Version 3.0 of the CompCert formally-verified C compiler is released. This is the first version of CompCert that fully supports 64-bit architectures, with pointers and memory addresses that can be either 32 or 64-bit wide. The existing x86 32-bit port was extended to generate x86 64-bit code as well.

Jean-Marie Madiot joins the Gallium team

Jean-Marie Madiot joins the Gallium team as an Inria chargé de recherche (research scientist). Welcome, Jean-Marie!

Van Wijngaarden Award

Mathematician Sara van de Geer and computer scientist Xavier Leroy receive the Van Wijngaarden Award 2016 from Centrum Wiskunde & Informatica, Amsterdam.

Ph.D. defense of Jacques-Henri Jourdan

Jacques-Henri Jourdan successfully defended his Ph.D. thesis, Verasco: a Formally Verified C Static Analyzer, at University Paris Diderot. Congratulations, Jacques-Henri!

Adrien Guatto joins the Gallium team

Adrien Guatto joins the Gallium team as a post-doctoral fellow on the ERC DeepSea project. Welcome, Adrien!

Ph.D. defense of Gabriel Scherer

Gabriel Scherer successfully defended his Ph.D. thesis, Which types have a unique inhabitant? Focusing on pure program equivalence at University Paris Diderot. Congratulations, Gabriel!

Most Influential POPL Paper Award

Xavier Leroy received the ACM SIGPLAN Most Influential POPL Paper Award for his POPL 2006 paper, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant.

New offices in Paris

Bye bye the Rocquencourt campus, we are now located in the new Inria offices in Paris 12e arrondissement. Come and visit us often, it is much easier to reach than the previous location!

Older news...
A quelques pas de lui
le gallium surfondu beurre de petits lits
avant de se tapir en la blende zinguée

Raymond Queneau,
Petite cosmogonie portative

See also

Inria web sites

Related project-teams

Activity reports of Gallium