leo (dot) lveb (at) gmail (dot) com
I am currently a PhD student in Computer Science at the IRIF laboratory in Paris. My supervisors are Paul-André Melliès in Paris and Lars Birkedal in Aarhus.
Draft: 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] (2020)
Draft: Concurrent separation logic meets template games with Paul-André Melliès (2020)
Paper: An Asynchronous Soundness Theorem for Concurrent Separation Logic with Paul-André Melliès (LICS'18)
During my internship in Aahrus, 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).