Background

I am currently a Postdoc, working on verified compilation and formal methods with Tobias Grosser at the University of Cambridge. I am currently working on the Lean-MLIR project, a formalisation of the MLIR intermediate representation using the Lean proof assistant.

• 2025-present: Postdoc at the University of Cambridge
• 2021-2024: Postdoc at MPI-SWS in Kaiserslautern, Germany, with Viktor Vafeiadis
• 2020-2021: ATER at Collège de France, in the Cambium project team
• 2017-2021: PhD student at IRIF
• 1-7/2017: Internship with Masahito Hasegawa at RIMS, Kyoto
• 9-12/2016: Internship in Lars Birkedal's group at Aarhus University
• 2015-2016: M2 at MPRI
• 2013-2015: L3&M1 at ENS Lyon

Papers & Drafts

• This paper introduces verified decision procedures for bitvectors with symbolic widths in the Lean proof assistant.

  Paper: Certified Decision Procedures for Width-Independent Bitvector Predicates, by Siddharth Bhat*, Leo Stefanesco*, Chris Hughes, and Tobias Grosser, (OOPSLA 2025)

• This paper describes bv_decide, a tactic to decide fixed-width bitvector problems in Lean.

  Paper: Interactive Bit Vector Reasoning using Verified Bitblasting with Henrik Böving et al, (OOPSLA 2025)

• 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).