The Gallium team has been replaced in 2019 withCambium.
At Gallium, we conduct research on the design, formalization andimplementation of programming languages and systems.TheOCamlfunctional language and theCompCert verified compiler embody many of our research results. Our objective is toimprove the reliability of software systems through:
Follow the links at the top of this page to learn more aboutwho we are and what we do.
Our studentArmaël Guéneau has defended his thesis on Monday, December 16, 2019.
The paperSpy 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.
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!
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.
Xavier Leroy's inaugural lecture at Collège de France,Le logiciel, entre l’esprit et la matière, is now available online, inthe original French and as apreliminary English translation.
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!
The paperFinding Missed Compiler Optimizations by Differential Testing, by Gergö Barany, received the best paper award at theCompiler Construction 2018 conference.
The following paper was accepted to PLDI 2018:Heartbeat Scheduling: Provable Efficiency for Nested Parallelismby Umut Acar, Arthur Charguéraud, Adrien Guatto, Mike Rainey, Filip Sieczkowski.
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.
The following paper will be presented at ICFP in Sept 2017:Visitors Unchained by François Pottier.
Jacques-Henri Jourdan receives the2016 award fromGDR Génie de la Programmation et du Logiciel for his PhD thesis,Verasco: a Formally Verified C Static Analyzer.
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 Gallium on a post-doc position. Welcome, Gergö!
Version 3.0 of theCompCert 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 as an Inriachargé de recherche (research scientist). Welcome, Jean-Marie!
MathematicianSara van de Geer and computer scientistXavier Leroy receive theVan Wijngaarden Award 2016 from Centrum Wiskunde & Informatica, Amsterdam.
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 as a post-doctoral fellow on the ERC DeepSea project. Welcome, Adrien!
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!
Xavier Leroyreceived theACM SIGPLAN Most Influential POPL Paper Awardfor his POPL 2006 paper,Formal certification of a compiler back-end, or: programming a compiler with a proof assistant.
Bye bye the Rocquencourt campus, we are now located in the newInria offices in Paris 12e arrondissement. Come and visit us often, it is much easier to reach than the previous location!