first (dot) last (at) cl.cam.ac.uk
I am currently a Postdoc, working on verified compilation and formal methods with Tobias Grosser at the Univerity of Cambridge. I am curently working on the Lean-MLIR project, a formalisation of the MLIR intermediate representation using the Lean proof assistant.
This paper presents a characterization of the MUST preorder, a notion of contextual refinement for programs communicating using message passing, in an asynchronous manner. I contributed mostly on the mechanization side, in particular a formalisation of bar induction for labeled transition systems.
Paper: Constructive characterisations of the must-preorder for asynchrony with Giovanni Bernardi, Ilaria Castellani, and Paul Laforgue, (ESOP'25)
An extension of the Iris program logic with a more intensional adequacy theorem which allows to construct simulations between a program and an abstract model. In particular, one can prove fair termination of concurrent programs.
Paper: Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement with Amin Timany, Simon Oddershede Gregersen, Jonas Kastberg Hinrichsen, Léon Gondelman, Abel Nieto and Lars Birkedal (POPL'24)
A framework for the specification of libraries that can exhibit weakly-consistent behaviors, as well as use persistent memory. This builds on the Yacovet framework, adding persistence.
Paper: Specifying and Verifying Persistent Libraries with Azalea Raad, Viktor Vafeiadis (ESOP'24)
PhD thesis: Asynchronous and Relational Soundness Theorems for Concurrent Separation Logic
Paper: Layered and Object-Based Game Semantics, with Arthur Oliveira Vale, Paul-André Mellies, Zhong Shao and Jérémie Koenig (POPL'22)
I visited the Mobility Reading Group at Imperial with funding from the FSMP in Spring 2019.
Draft: Game Semantics: Easy as Pi with Simon Castellan and Nobuko Yoshida
Paper: Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris with Paolo Giarrusso, Amin Timany, Lars Birkedal and Robbert Krebbers [Coq] (ICFP'20)
Paper: Concurrent separation logic meets template games with Paul-André Melliès (LiCS'20)
Paper: An Asynchronous Soundness Theorem for Concurrent Separation Logic with Paul-André Melliès (LICS'18)
During my internship in Aarhus, I worked on proving the safety of the ST monad using logical relations in Iris.
Paper: A Logical Relation for Monadic Encapsulation of State [Coq formalization] with Amin Timany, Morten Krogh-Jespersen and Lars Birkedal (POPL'18)
Summer 2016: Internship under the supervision of Paul-André Melliès at IRIF on Concurrent Separation Logic.
Paper: A Game Semantics of Concurrent Separation Logic, with P.-A. Melliès (MFPS'17)
In May 2015, I worked under the supervision of Gilles Barthe and Benedikt Schmidt at IMDEA Software on formal proofs of probabilistic algorithms
Paper: Relational reasoning via probabilistic coupling with Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub (LPAR 20).
During summer 2014, I worked under the supervision of David Pichardie and Delphine Demange at INRIA Rennes on implementing and proving a constant propagation pass on SSA to their extension of CompCert called CompCertSSA.
Internship report (in french): Compilation optimisante vérifiée sur forme SSA.
Paper: Verifying Fast and Sparse SSA-based Optimizations in Coq with Delphine Demange and David Pichardie (CC'15).