4 papers
Verifying Isolation Levels of Database Implementations for Free Using Separation Logic
Anders Alnor Mathiasen, Amin Timany, Lars Birkedal
Modern databases are highly concurrent and provide transactions as a mean of grouping several database operations into atomically applied units. Database vendors and software engin…
Yarrow: Reconciling Effect Handlers and Region-Based Memory Management
Anders Alnor Mathiasen, Amin Timany, Lars Birkedal
We present a new ML-like programming language Yarrow with algebraic effects and region-based memory management. Reconciling these programming language features into one language is…
Context-Dependent Effects and Concurrency in Guarded Interaction Trees
Sergei Stepanenko, Emma Nardino, Virgil Marionneau +3
Guarded Interaction Trees are a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Rocq. We present an extension of…
Reasoning about Weak Isolation Levels in Separation Logic
Anders Alnor Mathiasen, Léon Gondelman, Léon Ducruet +2
Consistency guarantees among concurrently executing transactions in local- and distributed systems, commonly referred to as isolation levels, have been formalized in a number of mo…