79 citations · 353 across the 23 of their papers we have counts for
28 papers
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…
Controlling unfolding in type theory
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli +2
We present a new way to control the unfolding of definitions in dependent type theory. Traditionally, proof assistants require users to fix whether each definition will or will not…
Denotational semantics of general store and polymorphism
Jonathan Sterling, Daniel Gratzer, Lars Birkedal
We contribute the first denotational semantics of polymorphic dependent type theory extended by an equational theory for general (higher-order) reference types and recursive types,…
Unifying cubical and multimodal type theory
Frederik Lerbjerg Aagaard, Magnus Baunsgaard Kristensen, Daniel Gratzer +1
In this paper we combine the principled approach to modalities from multimodal type theory (MTT) with the computationally well-behaved realization of identity types from cubical ty…
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…
Multimodal Dependent Type Theory
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts +1
We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transforma…
Client-Server Sessions in Linear Logic
Zesen Qian, G. A. Kavvos, Lars Birkedal
We introduce coexponentials, a new set of modalities for Classical Linear Logic. As duals to exponentials, the coexponentials codify a distributed form of the structural rules of w…
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
Dan Frumin, Robbert Krebbers, Lars Birkedal
We present a new version of ReLoC: a relational separation logic for proving refinements of programs with higher-order state, fine-grained concurrency, polymorphism and recursive t…
Compositional Non-Interference for Fine-Grained Concurrent Programs
Dan Frumin, Robbert Krebbers, Lars Birkedal
Non-interference is a program property that ensures the absence of information leaks. In the context of programming languages, there exist two common approaches for establishing no…
Modal Dependent Type Theory and Dependent Right Adjoints
Lars Birkedal, Ranald Clouston, Bassel Mannaa +3
In recent years we have seen several new models of dependent type theory extended with some form of modal necessity operator, including nominal type theory, guarded and clocked typ…
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…
Guarded Cubical Type Theory
Lars Birkedal, Aleš Bizjak, Ranald Clouston +3
This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guard…
Guarded Cubical Type Theory: Path Equality for Guarded Recursion
Lars Birkedal, Aleš Bizjak, Ranald Clouston +3
This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guard…
Guarded Dependent Type Theory with Coinductive Types
Aleš Bizjak, Hans Bugge Grathwohl, Ranald Clouston +2
We present guarded dependent type theory, gDTT, an extensional dependent type theory with a `later' modality and clock quantifiers for programming and proving with guarded recursiv…
Programming and Reasoning with Guarded Recursion for Coinductive Types
Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl +1
We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures th…
Step-Indexed Logical Relations for Probability (long version)
Aleš Bizjak, Lars Birkedal
It is well-known that constructing models of higher-order probabilistic programming languages is challenging. We show how to construct step-indexed logical relations for a probabil…
Step-Indexed Relational Reasoning for Countable Nondeterminism
Lars Birkedal, Aleš Bizjak, Jan Schwinghammer
Programming languages with countable nondeterministic choice are computationally interesting since countable nondeterminism arises when modeling fairness for concurrent systems. Be…
First steps in synthetic guarded domain theory: step-indexing in the topos of trees
Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer +1
We present the topos S of trees as a model of guarded recursion. We study the internal dependently-typed higher-order logic of S and show that S models two modal operators, on pred…
Two for the Price of One: Lifting Separation Logic Assertions
Jacob Thamsborg, Lars Birkedal, Hongseok Yang
Recently, data abstraction has been studied in the context of separation logic, with noticeable practical successes: the developed logics have enabled clean proofs of tricky challe…
Nested Hoare Triples and Frame Rules for Higher-order Store
Jan Schwinghammer, Lars Birkedal, Bernhard Reus +1
Separation logic is a Hoare-style logic for reasoning about programs with heap-allocated mutable data structures. As a step toward extending separation logic to high-level language…