leo (dot) stefanesco (at) ens-lyon (dot) fr
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)
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 Deplhine 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).