Compositional Higher-Order Reasoning about Distributed Systems (CHORDS)
ERC Advanced Grant: 101096090.
PI: Lars Birkedal, Aarhus University.
Starting date: September 2023.
Acknowledgments
Abstract
Publications
Free theorems from univalent reference types: The impact of univalence on denotational semantics
J. Sterling, D. Gratzer, and L. Birkedal
Submitted for publication.
.pdf
A Logical Approach to Type Soundness
A. Timany, R. Krebbers, D. Dreyer, and L. Birkedal.
Submitted for publication.
.pdf
Controlling unfolding in type theory
D. Gratzer, J. Sterling, C. Angiuli, T. Coquand, and L. Birkedal
Submitted for publication.
.pdf
Denotational semantics of general store and polymorphism
J. Sterling, D. Gratzer, and L. Birkedal
Submitted for publication.
.pdf
Unifying Cubical and Multimodal Type Theory
F.L. Aagaard, M.B. Kristensen, D. Gratzer, and L. Birkedal
Submitted for publication.
.pdf
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C
A. Gueneau, J. Hostert, S. Spies, M. Sammler, L. Birkedal, and D. Dreyer
In Proceedings of OOPSLA 2023.
.pdf
Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory
S. Vindum and L. Birkedal
In Proceedings of OOPSLA 2023.
.pdf
Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols
L. Gondelman, J. Hinrichsen, A. Timany, and L. Birkedal
In Proceedings of ICFP 2023.
.pdf
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
S.O. Gregersen, A. Aguirre, P. Haselwarter, J. Tassarotti, and L. Birkedal.
arXiv:2301.10061
.pdf
