3 papers
cs.DB2026
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…
cs.PL2026
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…
cs.PL2025
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…