Compositional Higher-Order Reasoning about Distributed Systems (CHORDS)

ERC Advanced Grant: 101096090.
PI: Lars Birkedal, Aarhus University.
European Research Council

Starting date: September 2023.

Acknowledgments

Abstract

Publications

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
K.H. Li, A. Aguirre, S.O. Gregersen, P.G. Haselwarter, J. Tassarotti, L. Birkedal.
In Proceedings of ICFP 2025.
.pdf
Reasoning about Weak Isolation Levels in Separation Logic
A. A. Mathiasen, L. Gondelman, L. Ducruet, A. Timany, L. Birkedal
In Proceedings of ICFP 2025.
.pdf
arXiv
Idempotent Resources in Separation Logic (The Heart of core in Iris)
D. Gratzer, M. A. Moeller, L. Birkedal
In Proceedings of FOSSACS 2025.
.pdf
Context-Dependent Effects in Guarded Interaction Trees
S. Stepanenko, E. Nardino, D. Frumin, A. Timany, L. Birkedal
In Proceedings of ESOP 2025.
.pdf
The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic
S. Vindum, A.L. Georges, L. Birkedal
In Proceedings of CPP 2025.
Recipient of CPP 2025 Distinguished Paper Award
.pdf
Modelling Recursion and Probabilistic Choice in Guarded Type Theory
P.J.A. Stassen, R.E. Møgelberg, M. Zwart, A. Aguirre, L. Birkedal
In Proceedings of POPL 2025.
.pdf
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
P.G. Haselwarter, K.H. Li, A. Aguirre, S.O. Gregersen, J. Tassarotti, L. Birkedal
In Proceedings of POPL 2025.
.pdf
Tachis: Higher-Order Separation Logic with Credits for Expected Costs
P. Haselwarter, Kh.H. Li., M. de Medeiros, S.O. Gregersen, A. Aguirre, J. Tassarotti, and L. Birkedal.
In Proceedings of OOPSLA 2024.
.pdf
Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly
M. Legoupil, J. Rousseau, A.L. Georges, J. Pichon-Pharabod, L. Birkedal
In Proceedings of OOPSLA 2024.
.pdf
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
A. Aguirre, P. Haselwarter, M. de Medeiros, K.H. Li., S.O. Gregersen, , J. Tassarotti, and L. Birkedal.
In Proceedings of ICFP 2024.
Recipient of ICFP 2024 Distinguished Paper Award
.pdf
Almost-Sure Termination by Guarded Refinement
S.O. Gregersen, A. Aguirre, P. Haselwarter, J. Tassarotti, and L. Birkedal.
In Proceedings of ICFP 2024.
.pdf
A Logical Approach to Type Soundness
A. Timany, R. Krebbers, D. Dreyer, and L. Birkedal.
Journal of the ACM, 2024.
.pdf
Controlling unfolding in type theory
D. Gratzer, J. Sterling, C. Angiuli, T. Coquand, and L. Birkedal
Accepted for publication in MSCS.
.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.
In Logical Methods in Computer Science, Vol 20, Issue 4, 2024.
.pdf
Modular Denotational Semantics for Effects with Guarded Interaction Trees
D. Frumin, A. Timany, and L. Birkedal.
In Proceedings of POPL 2024.
Recipient of POPL 2024 Distinguished Paper Award
.pdf
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
S.O. Gregersen, A. Aguirre, P.G. Haselwarter, J. Tassarotti, and L. Birkedal.
In Proceedings of POPL 2024.
.pdf
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
A. Hammon, Z. Liu, T. Perami, P. Sewell, L. Birkedal, and J. Pichon-Pharabod.
In Proceedings of POPL 2024.
.pdf
The Essence of Generalized Algebraic Data Types
F. Sieczkowski, S. Stepanenko, J. Sterling, and L. Birkedal.
In Proceedings of POPL 2024.
.pdf
The Logical Essence of Well-Bracketed Control Flow
A. Timany, A. Gueneau, and L. Birkedal.
In Proceedings of POPL 2024.
.pdf
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
A. Timany, S.O. Gregersen, L. Stefanesco, J.K. Hinrichsen, L. Gondelman, A. Nieto, and L. Birkedal.
In Proceedings of POPL 2024.
.pdf
Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics
J. Sterling, D. Gratzer, and L. Birkedal.
In Proceedings of CSL 2024.
.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