12 citations · 19 across the 9 of their papers we have counts for
11 papers
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…
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…
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…
Modular Denotational Semantics for Effects with Guarded Interaction Trees
Dan Frumin, Amin Timany, Lars Birkedal
We present guarded interaction trees -- a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Coq, inspired by domain…
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…
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit
Tobias Reinhard, Amin Timany, Bart Jacobs
Programs for multiprocessor machines commonly perform busy-waiting for synchronisation. In this paper, we make a first step towards proving termination of such programs. We approxi…
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report
Tobias Reinhard, Amin Timany, Bart Jacobs
Programs for multiprocessor machines commonly perform busy-waiting for synchronisation. In this paper, we make a first step towards proving termination of such programs. We approxi…
Abstract I/O Specification
Willem Penninckx, Amin Timany, Bart Jacobs
We recently proposed an approach for the specification and modular formal verification of the interactive (I/O) behavior of programs, based on an embedding of Petri nets into separ…
Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC)
Amin Timany, Matthieu Sozeau
In order to avoid well-know paradoxes associated with self-referential definitions, higher-order dependent type theories stratify the theory using a countably infinite hierarchy of…
Category Theory in Coq 8.5
Amin Timany, Bart Jacobs
We report on our experience implementing category theory in Coq 8.5. The repository of this development can be found at https://bitbucket.org/amintimany/categories/. This implement…