42 citations · 56 across the 5 of their papers we have counts for
8 papers
Constructive characterisations of the must-preorder for asynchrony
Giovanni Bernardi, Ilaria Castellani, Paul Laforgue +1
De Nicola and Hennessy's must-preorder is a contextual refinement which states that a server q refines a server p if all clients satisfied by p are also satisfied by q. Owing to th…
Specifying and Verifying Persistent Libraries
Léo Stefanesco, Azalea Raad, Viktor Vafeiadis
We present a general framework for specifying and verifying persistent libraries, that is, libraries of data structures that provide some persistency guarantees upon a failure of t…
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco +4
Expressive state-of-the-art separation logics rely on step-indexing to model semantically complex features and to support modular reasoning about imperative higher-order concurrent…
Game Semantics: Easy as Pi
Nobuko Yoshida, Simon Castellan, Léo Stefanesco
Game semantics has proven to be a robust method to give compositional semantics for a variety of higher-order programming languages. However, due to the complexity of most game mod…
Concurrent Separation Logic Meets Template Games
Paul-André Melliès, Léo Stefanesco
An old dream of concurrency theory and programming language semantics has been to uncover the fundamental synchronization mechanisms which regulate situations as different as game…
An Asynchronous soundness theorem for concurrent separation logic
Paul-André Melliès, Léo Stefanesco
Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. In this paper, we develop a concurrent and interactive a…
A Game Semantics of Concurrent Separation Logic
Paul-André Melliès, Léo Stefanesco
In this paper, we develop a game-theoretic account of concurrent separation logic. To every execution trace of the Code confronted to the Environment, we associate a specification…
Relational reasoning via probabilistic coupling
Gilles Barthe, Thomas Espitau, Benjamin Grégoire +3
Probabilistic coupling is a powerful tool for analyzing pairs of probabilistic processes. Roughly, coupling two processes requires finding an appropriate witness process that model…