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 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:
Follow the links at the top of this page to learn more about who we are and what we do.
Our student Armaël Guéneau has defended his thesis on Monday, December 16, 2019.
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.
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, in the original French and as a preliminary 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 paper Finding Missed Compiler Optimizations by Differential Testing, by Gergö Barany, received the best paper award at the Compiler Construction 2018 conference.
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.
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 the 2016 award from GDR 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 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 as an Inria chargé de recherche (research scientist). Welcome, Jean-Marie!
Mathematician Sara van de Geer and computer scientist Xavier Leroy receive the Van 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 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.
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!