8 citations · 8 across the 2 of their papers we have counts for
5 papers
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…
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…
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: 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…