A logical relation for monadic encapsulation of state: Proving contextual equivalences in the presence of runST A Timany, L Stefanesco, M Krogh-Jespersen, L Birkedal Proceedings of the ACM on Programming Languages 2 (POPL), 1-28, 2017 | 66 | 2017 |

Relational reasoning via probabilistic coupling G Barthe, T Espitau, B Grégoire, J Hsu, L Stefanesco, PY Strub Logic for Programming, Artificial Intelligence, and Reasoning: 20th …, 2015 | 37 | 2015 |

Verifying fast and sparse SSA-based optimizations in Coq D Demange, D Pichardie, L Stefanesco International Conference on Compiler Construction, 233-252, 2015 | 21 | 2015 |

Scala step-by-step: Soundness for DOT with step-indexed logical relations in Iris PG Giarrusso, L Stefanesco, A Timany, L Birkedal, R Krebbers Proceedings of the ACM on Programming Languages 4 (ICFP), 1-29, 2020 | 20 | 2020 |

Trillium: Unifying refinement and higher-order distributed separation logic A Timany, SO Gregersen, L Stefanesco, L Gondelman, A Nieto, L Birkedal arXiv preprint arXiv:2109.07863, 27, 2021 | 13 | 2021 |

Layered and object-based game semantics A Oliveira Vale, PA Melliès, Z Shao, J Koenig, L Stefanesco Proceedings of the ACM on Programming Languages 6 (POPL), 1-32, 2022 | 8 | 2022 |

Concurrent separation logic meets template games PA Melliès, L Stefanesco Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer …, 2020 | 7 | 2020 |

An Asynchronous Soundness Theorem for Concurrent Separation Logic PA Melliès, L Stefanesco Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer …, 2018 | 7 | 2018 |

A game semantics of concurrent separation logic PA Melliès, L Stefanesco Electronic Notes in Theoretical Computer Science 336, 241-256, 2018 | 6 | 2018 |

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement A Timany, SO Gregersen, L Stefanesco, JK Hinrichsen, L Gondelman, ... Proceedings of the ACM on Programming Languages 8 (POPL), 241-272, 2024 | 5 | 2024 |

Scala step-by-step: Soundness for DOT with step-indexed logical relations in Iris. PACMPL 4, ICFP (2020), 114: 1–114: 29 PG Giarrusso, L Stefanesco, A Timany, L Birkedal, R Krebbers | 5 | 2020 |

Game semantics: Easy as pi N Yoshida, S Castellan, L Stefanesco arXiv preprint arXiv:2011.05248, 2020 | 2 | 2020 |

Game semantics: Easy as pi S Castellan, L Stefanesco, N Yoshida arXiv preprint arXiv:2011.05248, 2020 | 2 | 2020 |

Scala Step-by-Step PG Giarrusso, L Stefanesco, A Timany, L Birkedal, R Krebbers Proceedings of the ACM on Programming Languages (PACMPL), 2020 | 1 | 2020 |

Specifying and Verifying Persistent Libraries L Stefanesco, A Raad, V Vafeiadis European Symposium on Programming, 185-211, 2024 | | 2024 |

Théorèmes de correction asynchrone et relationnelle de la logique de séparation concurrente L Stefanesco | | 2021 |

Asynchronous and relational soundness theorems for concurrent separation logic L Stefanesco Université de Paris, 2021 | | 2021 |

Concurrent Game Semantics: Easy as Pi S Castellan, L Stefanesco, N Yoshida Inria, 2020 | | 2020 |

Trillium: History-Sensitive Refinement in Separation Logic A TIMANY, SO GREGERSEN, LÉO STEFANESCO, L GONDELMAN, ... | | |

Internship: A formal proof of correctness of Tail-Recursion Modulo Constructor in the Iris logic L Stefanesco, F Pottier, G Scherer | | |