Armaël Guéneau defends
- 2019-12-16
Our student Armaël Guéneau has defended his thesis on Monday, December 16, 2019.
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
A paper at POPL 2020
- 2019-11-20
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
- 2019-11-20
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
- 2019-04-30
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
- 2019-04-30
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
- 2018-09-26
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
- 2018-02-24
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
- 2018-02-24
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
- 2017-11-03
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
- 2017-05-22
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
- 2017-05-17
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
- 2017-05-10
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
- 2017-03-01
Gergö Barany joins Gallium on a post-doc position. Welcome, Gergö!
CompCert 3.0 released, with full 64-bit support
- 2017-02-10
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
- 2017-01-03
Jean-Marie Madiot joins the Gallium team as an Inria chargé de recherche (research scientist). Welcome, Jean-Marie!
Van Wijngaarden Award
- 2016-11-02
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
- 2016-05-26
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
- 2016-04-01
Adrien Guatto joins the Gallium team as a post-doctoral fellow on the ERC DeepSea project. Welcome, Adrien!
Ph.D. defense of Gabriel Scherer
- 2016-03-30
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
- 2016-01-22
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
- 2016-01-15
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!