3 papers
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.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.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…