Verifying Fast and Sparse SSA-Based Optimizations in Coq. - Delphine Demange; David Pichardie; Léo Stefanesco (CC, 2015)

Relational Reasoning via Probabilistic Coupling. - Gilles Barthe; Thomas Espitau; Benjamin Grégoire; Justin Hsu; Léo Stefanesco; Pierre-Yves Strub (LPAR, 2015)

An Asynchronous Soundness Theorem for Concurrent Separation Logic. - Paul-André Melliès; Léo Stefanesco (LICS, 2018)

A Game Semantics of Concurrent Separation Logic. - Paul-André Melliès; Léo Stefanesco (MFPS, 2018)

A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST. - Amin Timany; Léo Stefanesco; Morten Krogh-Jespersen; Lars Birkedal (Proc. ACM Program. Lang., 2018)

Concurrent Separation Logic Meets Template Games. - Paul-André Melliès; Léo Stefanesco (LICS, 2020)

Game Semantics: Easy as Pi. - Nobuko Yoshida; Simon Castellan; Léo Stefanesco (CoRR, 2020)

Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris. - Paolo G. Giarrusso; Léo Stefanesco; Amin Timany; Lars Birkedal; Robbert Krebbers (Proc. ACM Program. Lang., 2020)

Trillium: Unifying Refinement and Higher-Order Distributed Separation Logic. - Amin Timany; Simon Oddershede Gregersen; Léo Stefanesco; Léon Gondelman; Abel Nieto; Lars Birkedal (CoRR, 2021)

Asynchronous and Relational Soundness Theorems for Concurrent Separation Logic. (Théorèmes de correction asynchrone et relationnelle de la logique de séparation concurrente). - Léo Stefanesco (2021)

Layered and object-based game semantics. - Arthur Oliveira Vale; Paul-André Melliès; Zhong Shao 001; Jérémie Koenig; Léo Stefanesco (Proc. ACM Program. Lang., 2022)

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement - Coq Artifact. - Amin Timany; Simon Oddershede Gregersen; Léo Stefanesco; Jonas Kastberg Hinrichsen; Léon Gondelman; Abel Nieto; Lars Birkedal (Zenodo, 2023)

Specifying and Verifying Persistent Libraries. - Léo Stefanesco; Azalea Raad; Viktor Vafeiadis (ESOP (2), 2024)

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement. - Amin Timany; Simon Oddershede Gregersen; Léo Stefanesco; Jonas Kastberg Hinrichsen; Léon Gondelman; Abel Nieto; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Constructive characterisations of the MUST-preorder for asynchrony. - Giovanni Bernardi 001; Ilaria Castellani; Paul Laforgue; Léo Stefanesco (ESOP (1), 2025)