8 citations · 8 across the 2 of their papers we have counts for
4 papers · 1 filter
A denotationally-based program logic for higher-order store
Frederik Lerbjerg Aagaard, Jonathan Sterling, Lars Birkedal
Separation logic is used to reason locally about stateful programs. State of the art program logics for higher-order store are usually built on top of untyped operational semantics…
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…
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus
Alejandro Aguirre, Gilles Barthe, Lars Birkedal +3
We extend the simply-typed guarded -calculus with discrete probabilities and endow it with a program logic for reasoning about relational properties of guarded probabilistic com…
Trace Properties from Separation Logic Specifications
Lars Birkedal, Thomas Dinsdale-Young, Guilhem Jaber +2
We propose a formal approach for relating abstract separation logic library specifications with the trace properties they enforce on interactions between a client and a library. Se…