first (dot) last (at) mpi-sws (dot) org
I am currently a Postdoc in Computer Science in Viktor Vafeiadis's group at the Max Planck Institute for Software Systems in Kaiserslautern, Germany.
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).