79 citations · 353 across the 23 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…
Towards univalent reference types
Jonathan Sterling, Daniel Gratzer, Lars Birkedal
We develop a denotational semantics for general reference types in an impredicative version of guarded homotopy type theory, an adaptation of synthetic guarded domain theory to Voe…
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…
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter +2
Probabilistic couplings are the foundation for many probabilistic relational program logics and arise when relating random sampling statements across two programs. In relational pr…