Publications of Lars Birkedal

Google Scholar entry DBLP entry

Chronological Listing (BibTeX database: BirkedalL.bib)

Iris in Lean
M. de Medeiros, S. Stepanenko, Z. Liu, O. Soeser, F. Leal, A. Tang, M. Vistrup, R. Jung, M. Carneiro, J. Tassarotti, M. Sammler, and L. Birkedal.
ArXiv
arXiv
Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic
M. de Medeiros, P. Liu, K.H. Li, A. Aguirre, L. Birkedal, and J. Tassarotti.
In Proceedings of LICS 2026.
pdf
Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic
P.G. Haselwarter, A. Aguirre, S. Gregersen, K.H. Li, J. Tassarotti, and L. Birkedal.
In Proceedings of PLDI 2026.
pdf
Cerisier: A Program Logic for Attestation in a Capability Machine
J. Rousseau, D. Carnier, T. Van Strydonck, S. Keuchel, D. Devriese, and L. Birkedal.
In Proceedings of PLDI 2026.
pdf
Iris-WasmFX: Modular Reasoning for Wasm Stack Switching
M. Legoupil, M. Pedersen, L. Birkedal, S. Lindley, and J. Pichon-Pharabod.
In Proceedings of PLDI 2026.
pdf
Contextual Refinement of Higher-Order Concurrent Probabilistic Programs
K.H. Li, A. Aguirre, J. Tassarotti, L. Birkedal.
In Proceedings of PLDI 2026.
pdf
Verifying Wait-Freedom for Concurrent Higher-Order Programs
E. Namakonov, L. Birkedal, and A. Timany.
In Proceedings of ECOOP 2026.
pdf
An Axiomatic Basis for Computer Programming on Relaxed Hardware Architectures: The AxSL Logics
Z. Liu, A. Hammond, T. Pérami, P. Sewell, L. Birkedal, and J. Pichon-Pharabod.
ACM Transactions on Programming Languages & Systems, Volume 48 Issue 1 (67 pp).
pdf
Mixtris: Mechanised Higher-Order Separation Logic for Mixed Choice Multiparty Message Passing
J. K. Hinrichsen, I. Quemerais, L. Birkedal.
In Proceedings of OOPSLA 2026.
pdf
Lawyer: Modular Obligations-Based Liveness Reasoning in Higher-Order Impredicative Concurrent Separation Logic
E. Namakonov, J. Fasse, B. Jacobs, L. Birkedal, and A. Timany.
In Proceedings of OOPSLA 2026.
pdf
Modular Speci!cations and Implementations of Random Samplers in Higher-Order Separation Logic
V. Marionneau, F. Sassus-Bourda, A. Aguirre, L. Birkedal.
In Proceedings of CPP 2026.
pdf
Contextual Refinement of Higher-Order Concurrent Probabilistic Programs
K.H. Li, A. Aguirre, J. Tassarotti, L. Birkedal.
ArXiv
arXiv
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
Controlling unfolding in type theory
D. Gratzer, J. Sterling, C. Angiuli, T. Coquand, and L. Birkedal
Mathematical Structures in Computer Science, Vol. 35, 38 pp., 2025.
.pdf publisher version
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
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.
Recipient of OOPSLA 2023 Distinguished Paper Award
.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
Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code
A.L. Georges, A. Gueneau, T. van Strydonck, A. Timany, A. Trieu, D. Devriese, and L. Birkedal
Journal of the ACM, 2024.
.pdf
mitten: A Flexible Multimodal Proof Assistant
P. Stassen, D. Gratzer, and L. Birkedal
In Proceedings of Types 2022 (LIPIcs, Volume 269, TYPES 2022).
.pdf
Modular Verification of State-Based CRDTs in Separation Logic.
A. Nieto, A. Daby-Seesaram, L. Gondelman, A. Timany, and L. Birkedal
In Proceedings of ECOOP 2023.
.pdf
A denotationally-based program logic for higher-order store.
F.L. Aagaard, J. Sterling, and L. Birkedal
In Proceedings of MFPS 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
Iris-Wasm: Robust and Modular Verification of WebAssembly Programs
X. Rao, A.L. Georges, M. Legoupil, C. Watt, J. Pichon-Pharabod, P. Gardner, and L. Birkedal
In Proceedings of PLDI 2023.
.pdf
VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A.
Zongyuan Liu, Sergei Stepanenko, Jean Pichon-Pharabod, Amin Timany, Aslan Askarov, Lars Birkedal.
In Proceedings of PLDI 2023.
.pdf
Step-Indexed Logical Relations for Nondeterministic and Probabilistic Choice
A. Aguirre and L. Birkedal
In Proceedings of POPL 2023.
.pdf
Modular Verification of Op-Based CRDTs in Separation Logic
A. Nieto, L. Gondelman, A. Reynaud, A.Timany, and L. Birkedal
In Proceedings of OOPSLA 2022.
.pdf
Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities
A.L. Georges, A. Trieu, and L. Birkedal
In Proceedings of OOPSLA 2022.
Recipient of OOPSLA 2022 Distinguished Paper Award
.pdf
Later Credits: Resourceful Reasoning for the Later Modality
S. Spies, L. Gaher, J. Tassarotti, R. Jung, R. Krebbers, L. Birkedal, and D. Dreyer.
In Proceedings of ICFP 2022.
.pdf
A Stratified Approach to Loeb Induction
D. Gratzer and L. Birkedal
In Proceedings of FSCD 2022.
.pdf errata.pdf
Modalities and Parametric Adjoints
D. Gratzer, E. Cavallo, G.A. Kavvos, A. Guatto, and L. Birkedal.
ACM Transactions on Computational Logic, 23:3, pp. 18:1–-18:29, 2022.
.pdf
Mechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Library
S.F. Vindum, D. Frumin, and L. Birkedal
In CPP 2022: Certified Proofs and Programs.
.pdf
Proving Full-System Security Properties under Multiple Attacker Models on Capability Machines.
T. Van Strydonck, A.L. Georges, A. Gueneau, A. Trieu, A. Timany, F. Piessens, L. Birkedal, and D. Devriese.
In CSF 2022: Computer Security Foundations
.pdf
Theorems for Free from Separation Logic Specifications
L. Birkedal, T. Dinsdale-Young, A. Gueneau, G. Jaber, K. Svendsen and N. Tzevelekos
In ICFP 2021: International Conference on Functional Programming
Recipient of ICFP 2021 Distinguished Paper Award
.pdf
Client-Server Sessions in Linear Logic
Z. Qian, A.G. Kavvos and L. Birkedal
In ICFP 2021: International Conference on Functional Programming
Recipient of ICFP 2021 Distinguished Paper Award
.pdf errata.pdf
Multimodal Dependent Type Theory
D. Gratzer, G.A. Kavvos, A. Nuyts, and L. Birkedal
Logical Methods in Computer Science 17:3, 2021. Journal version of LICS 2020 paper.
.pdf
Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic
S. Spies, L. Gaher, D. Gratzer, J. Tassarotti, R. Krebbers, D. Dreyer, and L. Birkedal
In PLDI 2021: Programming Language Design and Implementation
.pdf
Cap’ ou pas cap’ ? Preuve de programmes pour une machine a capacites en presence de code inconnu
A.L. Georges, A. Gueneau, T. van Strydonck, A. Timany, A. Trieu, D. Devriese, and L. Birkedal
In JFLA'21: Journees Francophones des Langages Applicatifs.
Tutorial-style simplified version of POPL 2021 paper.
.pdf
Contextual Refinement of the Michael-Scott Queue (Proof Pearl)
S.F. Vindum and L. Birkedal
In CPP 2021: Certified Proofs and Programs.
.pdf
Reasoning About Monotonicity in Separation Logic
A. Timany and L. Birkedal
In CPP 2021: Certified Proofs and Programs.
[amended after publication].pdf
Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
L. Gondelman, S.O. Gregersen, A. Nieto, A. Timany, and L. Birkedal
In POPL 2021: Principles of Programming Languages.
.pdf
Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
A.L. Georges, A. Gueneau, T. van Strydonck, A. Timany, A. Trieu, S. Huyghebaert, D. Devriese, and L. Birkedal
In POPL 2021: Principles of Programming Languages.
.pdf
Mechanized Logical Relations for Termination-Insensitive Noninterference
S.O. Gregersen, J. Bay, A. Timany, and L. Birkedal
In POPL 2021: Principles of Programming Languages.
.pdf
StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation using Linear Capabilities
L. Skorstengaard, D. Devriese, and L. Birkedal
Extended version of POPL 2019 paper. Journal of Functional Programming 31, E9, 2021.
.pdf
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
D. Frumin, R. Krebbers, L. Birkedal
Logical Methods in Computer Science 17:3, 2021. Extended version of LICS 2018.
.pdf website Coq development
Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris
P.G. Giarrusso, L. Stefanesco, A. Timany, L. Birkedal, R. Krebbers
In ICFP 2020: International Conference on Functional Programming
.pdf website Coq development
Compositional Non-Interference for Fine-Grained Concurrent Programs
D. Frumin, R. Krebbers, and L. Birkedal
In S&P 2021: Security and Privacy (Oakland)
[preprint] .pdf Coq development
Multimodal Dependent Type Theory
D. Gratzer, G. A. Kavvos, A. Nuyts, and L. Birkedal
In LICS 2020: Logic in Computer Science
.pdf
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems
M. Krogh-Jespersen, A. Timany, M.E. Ohlenbusch, S.O. Gregersen, and L. Birkedal
In ESOP 2020: European Symposium on Programming, Dublin, Ireland
.pdf technical appendix Coq development
Mechanized Reasoning about a Capability Machine
A.L. Georges, A. Trieue, and L. Birkedal
Extended Abstract for talk at PRISC 2020: Principles of Secure Compilation
.pdf
Implementing a Modal Dependent Type Theory
D. Gratzer, J. Sterling, and L. Birkedal
In ICFP 2019: International Conference on Functional Programming, Berlin, Germany
Recipient of ICFP 2019 Distinguished Paper Award
.pdf technical appendix
Mechanized Relational Verification of Concurrent Programs with Continuations
A. Timany and L. Birkedal
In ICFP 2019: International Conference on Functional Programming, Berlin, Germany
.pdf
Modal Dependent Type Theory and Dependent Right Adjoints
L. Birkedal, R. Clouston, B. Mannaa, R.E. Møgelberg, A.M. Pitts, and B. Spitters
Mathematical Structures in Computer Science 1-21, 2019
.pdf
Iron: Managing Obligations in Higher-Order Concurrent Separation Logic
A. Bizjak, D. Gratzer, R. Krebbers, and L. Birkedal
In POPL 2019: Principles of Programming Languages
.pdf
StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation using Linear Capabilities
L. Skorstengaard, D. Devriese, and L. Birkedal
In POPL 2019: Principles of Programming Languages
.pdf
Guarded Cubical Type Theory
L. Birkedal, A. Bizjak, R. Clouston, H.B. Grathwohl, B. Spitters, and A. Vezzosi
Journal of Automated Reasoning 63(2): 211--253, 2019
.pdf
Reasoning about a Capability Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management
L. Skorstengaard, D. Devriese, and L. Birkedal
ACM Transactions on Programming Languages (TOPLAS): 5, 2019
.pdf
ReLoC: a Mechanised Relational Logic for Fine-Grained Concurrency
D. Frumin, R. Krebbers, and L. Birkedal
In LICS 2018: Logic in Computer Science
.pdf
Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic
R. Jung, R. Krebbers, J-H. Jourdan, A. Bizjak, L. Birkedal, and D. Dreyer
Journal of Functional Programming, 28, 2018
Recipient of 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation from European Association for Theoretical Computer Science.
.pdf
A Model of Guarded Recursion via Generalised Equilogical Spaces
A. Bizjak and L. Birkedal
Theoretical Computer Science, 772:1–18, 2018
.pdf
Compositional Non-Interference for Concurrent Programs via Separation and Framing
A. Karbyshev, K. Svendsen, A. Askarov, and L. Birkedal
In POST 2018: Principles of Security and Trust
.pdf
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus
A. Aguirre, G. Barthe, L. Birkedal, A. Bizjak, M. Gaboardi, and D. Garg
In ESOP 2018: European Symposium on Programming
.pdf
Reasoning about a Capability Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management (without OS support)
L. Skorstengaard, D. Devriese, and L. Birkedal
In ESOP 2018: European Symposium on Programming
.pdf technical appendix
A Logical Relation for Monadic Encapsulation of State: Proving Contextual Equivalences in the Presence of runST
A. Timany, L. Stefanesco, M. Krogh-Jespersen, and L. Birkedal
In POPL 2018: Principles of Programming Languages
.pdf
On Models of Higher-Order Separation Logic
A. Bizjak and L. Birkedal
In MFPS 2017: Mathematical Foundations of Programming Semantics
.pdf
The Essence of Higher-Order Concurrent Separation Logic
R. Krebbers, R. Jung, A. Bizjak, J.-H. Jourdan, D. Dreyer, and L. Birkedal
In ESOP 2017: European Symposium on Programming
Recipient of 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation from European Association for Theoretical Computer Science.
.pdf
Caper: Automatic Verification for Fine-Grained Concurrency
T. Dinsdale-Young, P. Pinto, K.J. Andersen, and L. Birkedal
In ESOP 2017: European Symposium on Programming
.pdf
A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic
M. Krogh-Jespersen, K. Svendsen, and L. Birkedal
In POPL 2017: Principles of Programming Languages
.pdf
Interactive Proofs in Higher-Order Concurrent Separation Logic
R. Krebbers, A. Timany, and L. Birkedal
In POPL 2017: Principles of Programming Languages
.pdf
Guarded Cubical Type Theory: Path Equality for Guarded Recursion
L. Birkedal, A. Bizjak, R. Clouston, H.B. Grathwohl, B. Spitters, and A. Vezzosi
In CSL 2016: Computer Science Logic
.pdf
Higher-Order Ghost State
R. Jung, R. Krebbers, L. Birkedal, and D. Dreyer.
In ICFP 2016: International Conference on Functional Programming
Recipient of 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation from European Association for Theoretical Computer Science.
.pdf
The Guarded Lambda Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
R. Clouston, A. Bizjak, H. Bugge Grathwohl, and L. Birkedal
Logical Methods in Computer Science, 2016.
Journal version of FOSSACS 2015 paper
.pdf
A Kripke Logical Relation for Effect-Based Program Transformations
L. Birkedal, G. Jaber, F. Sieczkowski, and J. Thamsborg
Information and Computation, 2016
.pdf
Guarded Cubical Type Theory
L. Birkedal, A. Bizjak, R. Clouston, H.B. Gratwohl, B. Spitters, and A. Vezzosi.
In TYPES 2016
.pdf
Transfinite Step-Indexing: Decoupling Concrete and Logical Steps
K. Svendsen, F. Sieczkowski, and L. Birkedal
In ESOP 2016: European Symposium on Programming
.pdf
Guarded Dependent Type Theory with Coinductive Types
A. Bizjak, H.B. Grathwohl, R. Clouston, R.E. Møgelberg, and L. Birkedal
In FOSSACS 2016: Foundations of Software Science and Computation Structures
.pdf
Reasoning about Object Capabilities with Logical Relations and Effect Parametricity
D. Devriese, F. Piessens, and L. Birkedal
In EuroS&P 2016: European Symposium on Security and Privacy
.pdf
Verifying Custom Synchronisation Constructs using Higher-Order Separation Logic
M. Dodds, S. Jagannathan, M.J. Parkinson, K. Svendsen, and L. Birkedal
ACM Transactions on Programming Languages and Systems (TOPLAS), 38(2:4), 2016
.pdf
A Model of PCF in Guarded Type Theory
M. Paviotti, R.E. Møgelberg, and L. Birkedal
In MFPS 2015: Mathematical Foundations of Programming Semantics
.pdf
ModuRes: a Coq library for Modular Reasoning about Concurrent Higher-Order Imperative Programming Languages
F. Sieczkowski, A. Bizjak, and L. Birkedal
In ITP 2015: International Conference on Theorem Proving
.pdf
Step-indexed Logical Relations for Probability
A. Bizjak, and L. Birkedal
In FOSSACS 2015: Foundations of Software Science and Computation Structures
.pdf
Programming and Reasoning with Guarded Recursion for Coinductive Types
R. Clouston, A. Bizjak, H. Bugge Grathwohl, and L. Birkedal
In FOSSACS 2015: Foundations of Software Science and Computation Structures
.pdf
A Separation Logic for Fictional Sequential Consistency
F. Sieczkowski, K. Svendsen, L. Birkedal, and J. Pichon-Pharapod
In ESOP 2015: European Symposium on Programming
.pdf
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
R. Jung, D. Swasey, F. Sieczkowski, K. Svendsen, A. Turon, L. Birkedal, and D. Dreyer
In POPL 2015: Principles of Programming Languages
Recipient of Most Influential Paper Award at POPL 2025.
Recipient of 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation from European Association for Theoretical Computer Science.
.pdf
A Model of Countable Nondeterminism in Guarded Type Theory
A. Bizjak, L. Birkedal, and M. Miculan
In TLCA 2014: Typed Lambda Calculus and Applications
.pdf
Impredicative Concurrent Abstract Predicates
K. Svendsen and L. Birkedal
In ESOP 2014: European Symposium on Programming
.pdf
Step-Indexed Relational Reasoning for Countable Nondeterminism
L. Birkedal, A. Bizjak, and J. Schwinghammer
Logical Methods in Computer Science, 9(4):1–23, October 2013.
.pdf
Unifying Refinement and Hoare-Style Reasoning in a Logic for Higher-Order Concurrency
A. Turon, D. Dreyer, and L. Birkedal
In ICFP 2013: International Conference on Functional Programming
.pdf
Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes
L. Birkedal and R.E. Møgelberg
In LICS 2013: Logic in Computer Science
.pdf
Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library
K. Svendsen, L. Birkedal, and M. Parkinson
In ECOOP 2013: European Conference on Object-Oriented Programming
.pdf
Modular Reasoning about Separation of Concurrent Data Structures
K. Svendsen, L. Birkedal, and M. Parkinson
In ESOP 2013: European Symposium on Programming
.pdf
A Note on the Transitivity of Step-Indexed Logical Relations
Lars Birkedal and Ales Bizjak
Manuscript, 2012
.pdf
Logical Relations for Fine-Grained Concurrency
A. Turon, J. Thamsborg, A. Ahmed, L. Birkedal, and D. Dreyer
In POPL 2013: Principles of Programming Languages
.pdf
Views: Compositional Reasoning for Concurrency
T. Dinsdale-Young, L. Birkedal, P. Gardner, M. Parkinson, and H. Yang
In POPL 2013: Principles of Programming Languages
Recipient of Most Influential Paper Award at POPL 2023
.pdf
First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees
L. Birkedal, R. Møgelberg, J. Schwinghammer, and K. Støvring
Logical Methods in Computer Science, 8(4), October 2012.
.pdf
Two for the Price of One: Lifting Separation Logic Assertions
J. Thamsborg, L. Birkedal, and H. Yang
Logical Methods in Computer Science, 8(3), September 2012.
.pdf
A Concurrent Logical Relation
L. Birkedal, F. Sieczkowski, and J. Thamsborg
In CSL 2012: Computer Science Logic
.pdf
Charge! a Framework for Higher-Order Separation Logic in Coq
J. Bengtson, J.B. Jensen, and L. Birkedal
In ITP 2012: International Conference on Theorem Proving
.pdf
A Relational Realizability Model for Higher-Order Stateful ADTs
L. Birkedal, K. Støvring, and J. Thamsborg
Journal of Logic and Algebraic Programming, 81(4):491–521,
.pdf
The Impact of Higher-Order State and Control Effects on Local Relational Reasoning
D. Dreyer, G. Neis, and L. Birkedal
Journal of Functional Programming, February 2012.
.pdf
A Step-Indexed Kripke Model of Hidden State
J. Schwinghammer, L. Birkedal, F. Pottier, B. Reus, K. Støvring, and H. Yang
Mathematical Structures in Computer Science, 2012.
.pdf
Fictional Separation Logic
J.B. Jensen and L. Birkedal
In ESOP 2012: European Symposium on Programming
.pdf
Formalized Verification of Snapshotable Trees: Separation and Sharing
H. Mehnert, F. Sieczkowski, L. Birkedal, and P. Sestoft
In VSTTE 2012: Verifiec Software, Theories, Toools, and Experiments
.pdf
An Inductive Characterization of Matching in Binding Bigraphs
T.C. Damgaard, A.J. Glenstrup, L. Birkedal, and R. Milner
Formal Aspects of Computing 2012
.pdf
Step-Indexed Relational Reasoning for Countable Nondeterminism
J. Schwinghammer and L. Birkedal
In CSL 2011: Computer Science Logic
.pdf
A Step-Indexed Kripke Model of Separation Logic for Storable Locks
A. Buisse, L. Birkedal, and K. Støvring
In MFPS 2011: Mathematical Foundations of Programming Semantics
.pdf
A Kripke Logical Relation for Effect-Based Program Transformations
J. Thamsborg and L. Birkedal
In ICFP 2011: International Conference on Functional Programming
.pdf
Nested Hoare Triples and Frame Rules for Higher-Order Store
J. Schwinghammer, L. Birkedal, B. Reus, and H. Yang
Logical Methods in Computer Science, 7(3:21), July 2011.
.pdf
Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq
J. Bengtson, J.B. Jensen, F. Sieczkowski, and L. Birkedal
In ITP 2011: International Conference on Theorem Proving
.pdf
Partiality, State, and Dependent Types
K. Svendsen, L. Birkedal, and A. Nanevski
In TLCA 2011: Typed Lambda Calculus and Applications
.pdf
First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees
L. Birkedal, R. Møgelberg, J. Schwinghammer, and K. Støvring
In LICS 2011: Logic in Computer Science
.pdf
Logical Step-Indexed Logical Relations
D. Dreyer, A. Ahmed, and L. Birkedal
Logical Methods in Computer Science, 7(2:16), June 2011.
.pdf
A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces
J. Schwinghammer, L. Birkedal, and K. Støvring
In FOSSACS 2011: Foundations of Software Science and Computation Structures
.pdf
Step-Indexed Kripke Models over Recursive Worlds
L. Birkedal, B. Reus, J. Schwinghammer, K. Støvring, J. Thamsborg, and H. Yang
In POPL 2011: Principles of Programming Languages
.pdf
The Category-Theoretic Solution of Recursive Metric-Space Equations
L. Birkedal, K. Støvring, and J. Thamsborg
Theoretical Computer Science, 411:4102–4122, 2010.
.pdf
Formalizing Domains, Ultrametric Spaces and Semantics of Programming Languages
N. Benton, L. Birkedal, A. Kennedy, and C. Varming
Manuscript, 2010.
.pdf coq
A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces
L. Birkedal, J. Schwinghammer, and K. Støvring
In FICS 2012: Fixed Points in Computer Science
.pdf
A Metric Model of Guarded Recursion
L. Birkedal, J. Schwinghammer, and K. Støvring
In FICS 2012: Fixed Points in Computer Science
.pdf
Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
L. Birkedal, K. Støvring, and J. Thamsborg
Mathematical Structures in Computer Science, May 2010.
.pdf
The Impact of Higher-Order State and Control Effects on Local Relational Reasoning
D. Dreyer, G. Neis, and L. Birkedal
In ICFP 2010: International Conference on Functional Programming
.pdf
Modular Verification of Linked Lists with Views via Separation Logic
J.B. Jensen, L. Birkedal, and P. Sestoft
In FTfJP 2010: Formal Techniques for Java-like Programs
.pdf
Verifying Generics and Delegates
K. Svendsen, L. Birkedal, and M. Parkinson
In ECOOP 2010: European Conference on Object-Oriented Programming
.pdf
Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
L. Birkedal, K. Støvring, and J. Thamsborg
Technical Report TR-2010-124, IT University of Copenhagen, January 2010.
.pdf
A Semantic Foundation for Hidden State
J. Schwinghammer, H. Yang, L. Birkedal, F. Pottier, and B. Reus
In FOSSACS 2010: Foundations of Software Science and Computation Structures
.pdf
Verifying Event-Driven Programs using Ramified Frame Properties
N. Krishnaswami, L. Birkedal, and J. Aldrich
In TLDI 2010: Types in Language Design and Implementation
.pdf
The Category-Theoretic Solution of Recursive Metric-Space Equations
L. Birkedal, K. Støvring, and J. Thamsborg
Technical Report ITU-2009-119, IT University of Copenhagen, 2009.
.pdf
A Relational Modal Logic for Higher-Order Stateful ADTs
D. Dreyer, G. Neis, A. Rossberg, and L. Birkedal
In POPL 2010: Principles of Programming Languages
.pdf
Solutions of Generalized Recursive Metric-Space Equations
L. Birkedal, K. Støvring, and J. Thamsborg
In FICS 2009: Fixed Points in Computer Science
.pdf
Logical Step-Indexed Logical Relations
D. Dreyer, A. Ahmed, and L. Birkedal
In LICS 2009: Logic in Computer Science
.pdf
Nested Hoare Triples and Frame Rules for Higher-Order Store
In CSL 2009: Computer Science Logic
place
.pdf
Higher-Order Contexts via Games and the Int-Construction
L. Birkedal, M. Bundgaard, S. Debois, T. Hildebrandt, and D. Grohmann
Technical Report ITU-TR-2009-117, IT University of Copenhagen, 2009.
.pdf
Realizability Semantics of Parametric Polymorphism, References, and Recursive Types
L. Birkedal, K. Støvring, and J. Thamsborg
In FOSSACS 2009: Foundations of Software Science and Computation Structures
.pdf
Relational Parametricity for References and Recursive Types
L. Birkedal, K. Støvring, and J. Thamsborg
In TLDI 2009: Types in Language Design and Implementation
.pdf
Design Patterns in Separation Logic
N. Krishnaswami, J. Aldrich, L. Birkedal, K. Svendsen, and A. Buisse
In TLDI 2009: Types in Language Design and Implementation
.pdf
Verifying Design Patterns in Hoare Type Theory
K. Svendsen, A. Buisse, and L. Birkedal
Technical Report ITU-TR-2008-112, IT University of Copenhagen, September 2008.
.pdf
Ynot: Dependent Types for Imperative Programs
A. Nanevski, G. Morrisett, A. Shinnar, P. Goverau, and L. Birkedal
In ICFP 2008: International Conference on Functional Programming
.pdf
On the Construction of Sorted Bigraphical Reactive Systems
L. Birkedal, S. Debois, and T. Hildebrandt
In CONCUR 2008: International Conference on Concurrency
.pdf
Category-theoretic models of Linear Abadi & Plotkin Logic
L. Birkedal, R.E. Møgelberg, and R.L. Petersen
Theory and Applications in Categories, 20(7):116–151, 2008.
.pdf
Synthetic Domain Theory and Models of Linear Abadi & Plotkin Logic
R.E. Møgelberg, L. Birkedal, and G. Rosolini
Annals of Pure and Applied Logic, 2008.
.pdf
A Simple Model of Separation Logic for Higher-order Store
L. Birkedal, B. Reus, J. Schwinghammer, and H. Yang
In ICALP 2008: International Colloquium on Automata, Languages, and Programming
.pdf
Higher-Order Separation Logic in Isabelle/HOLCF
C. Varming and L. Birkedal
In MFPS 2008: Mathematical Foundations of Programming Semantics
.pdf
A Realizability Model of Impredicative Hoare Type Theory
R.L. Petersen, L. Birkedal, A. Nanevski, and G. Morrisett
In ESOP 2008: European Symposium on Programming
.pdf
Domain-Theoretic Models of Parametric Polymorphism
L. Birkedal, R.E. Møgelberg, and R.L. Petersen
Theoretical Computer Science, 388(1–3):152–172, 2007.
.pdf
An Implementation of Bigraph Matching
A.J. Glenstrup, T.C. Damgaard, L. Birkedal, and E. Højsgaard
Manuscript, 2007
.pdf
Hoare Type Theory, Polymorphism and Separation
A. Nanevski, G. Morrisett, and L. Birkedal
Journal of Functional Programming, 2007.
.pdf
Modular Verification of the Subject-Observer Pattern via Higher-Order Separation Logic
N. Krishnaswami, J. Aldrich, and L. Birkedal
In FTfjP 2007: Formal Techniques for Java-like Programs
.pdf
BI-Hyperdoctrines, Higher-Order Separation Logic, and Abstraction
B. Biering, L. Birkedal, and N. Torp-Smith
ACM Transactions on Programming Languages and Systems (TOPLAS), 2007.
.pdf
Matching of Bigraphs
L. Birkedal, T.C. Damgaard, A. Glenstrup, and R. Milner
In Graph Transformation for Verification and Concurrency 2006
.pdf
Relational Parametricity and Separation Logic
L. Birkedal and H. Yang
In FOSSACS 2007: Foundations of Software Science and Computation Structures
.pdf
Abstract Predicates and Mutable ADTs in Hoare Type Theory
A. Nanevski, A. Ahmed, G. Morrisett, and L. Birkedal
In ESOP 2007: European Symposium on Programming
.pdf
Linear Abadi and Plotkin Logic
L. Birkedal, R.E. Møgelberg, and R.L. Petersen
Logical Methods in Computer Science, 2(5:2), August 2006.
.pdf
Semantics of Separation-Logic Typing and Higher-Order Frame Rules for Algol-like Languages
L. Birkedal, N. Torp-Smith, and H. Yang
Logical Methods in Computer Science, 2(5:1), August 2006.
.pdf
Local Reasoning about a Copying Garbage Collector
N. Torp-Smith, L. Birkedal, and J.C. Reynolds
ACM Transactions on Programming Languages and Systems (TOPLAS), 2006.
.pdf
Polymorphism and Separation in Hoare Type Theory
A. Nanevski, G. Morrisett, and L. Birkedal
In ICFP 2006: International Conference on Functional Programming
.pdf
Sortings for Reactive Systems
L. Birkedal, S. Debois, and T. Hildebrandt
In CONCUR 2006: International Conference on Concurrency Theory
.pdf
Relational Reasoning for Recursive Types and References
N. Bohr and L. Birkedal
In APLAS 2006: Asian Symposium on Programming Languages and Systems
.pdf
Operational Semantics and Models of Linear Abadi & Plotkin Logic
L. Birkedal, R.L. Petersen, R. Møgelberg, and C. Varming
Manuscript, 2006
.pdf
Matching of Bigraphs
L. Birkedal, T.C. Damgaard, A. Glenstrup, and R. Milner
Technical Report ITU-TR-2006-88, IT University of Copenhagen, June 2006.
.pdf
Axiomatizing Binding Bigraphs
T.C. Damgaard and L. Birkedal
Nordic Journal of Computing, 13(1-2):58–77, 2006.
.pdf
Bigraphical Programming Langauges for Pervasive Computing
L. Birkedal, M. Bundgaard, T.C. Damgaard, S. Debois, E. Elsborg, A.J. Glenstrup, T. Hildebrandt, R. Milner, and H. Niss
In International Workshop on Combining Theory and Systems Building in Pervasive Computing. Position Paper, 2006.
.pdf
Bigraphical Models of Context-aware Systems
L. Birkedal, S. Debois, E. Elsborg, T. Hildebrandt, and H. Niss
In FOSSACS 2006: Foundations of Software Science and Computation Structures
.pdf
BI-Hyperdoctrines, Higher-Order Separation Logic and Abstraction
B. Biering, L. Birkedal, and N. Torp-Smith
Technical Report ITU-TR-2005-69, IT University of Copenhagen, July 2005
.pdf
Categorical Models of Abadi-Plotkin's Logic for Parametricity
L. Birkedal and R.E. Møgelberg.
Mathematical Structures in Computer Science, 15:709–772, 2005.
.pdf
Parametric Domain-Theoretic Models of Polymorphic Intuitionistic / Linear Lambda Calculus
L. Birkedal, R.E. Møgelberg, and R.L. Petersen
IN MFPS 2005: Mathematical Foundations of Programming Semantics
.pdf
Synthetic Domain Theory and Models of Linear Abadi and Plotkin Logic
R.E. Møgelberg, L. Birkedal, and G. Rosolini
In MFPS 2005: Mathematical Foundations of Programming Semantics
.pdf
Parametric Domain-Theoretic Models of Linear Abadi-Plotkin Logic
L. Birkedal, R.E. Møgelberg, and R.L. Petersen
Technical Report TR-2005-57, IT University of Copenhagen, 2005.
.pdf
Synthetic Domain Theory and Models of Linear Abadi and Plotkin Logic
R.E. Møgelberg, L. Birkedal, and G. Rosolini
Technical Report TR-2005-59, IT University of Copenhagen, February 2005.
.pdf
Categorical models of PILL
R.E. Møgelberg, L. Birkedal, and R.L. Petersen
Technical Report TR-2005-58, IT University of Copenhagen, February 2005.
.pdf
Semantics of Separation-Logic Typing and Higher-Order Frame Rules
L. Birkedal, N. Torp-Smith, and H. Yang
In LICS 2005: Logic in Computer Science
.pdf
BI-Hyperdoctrines and Higher-Order Separation Logic
B. Biering, L. Birkedal, and N. Torp-Smith
In ESOP 2005: European Symposium on Programming
.pdf
An Infrastructure for Context-Dependent Mobile Multimedia Communication
J.Aa. Sørensen, K.J. Kristoffersen, A. Cervera, M. Schiøtz, T. Lynge, Z. Safar, and L. Birkedal
In IEEE International Workshop on Multimedia Signal Processing 2004.
.pdf
Bigraphical Programming Languages - a LaCoMoCo Research Project
L. Birkedal
In 2nd UK-Ubinet Workshop, Cambridge, UK, May 2004. Position Paper.
.pdf
On the Definition of Parametricity
L. Birkedal and R.E. Møgelberg
Technical Report 44, The IT University of Copenhagen, 2004.
.pdf
A Retrospective on Region-Based Memory Management
M. Tofte, L. Birkedal, M. Elsman, and N. Hallenberg
Higher Order Symbolic Computation, 17(2), 2004.
.pdf
Local Reasoning about a Copying Garbage Collector
L. Birkedal, N. Torp-Smith, and J.C. Reynolds
In POPL 2004: Principles of Programming Languages
.pdf
A General Notion of Realizability
L. Birkedal
Bulletin of Symbolic Logic, 8(2):266–282, 2002.
.pdf
Programming with Regions in the ML Kit (for Version 4)
M. Tofte, L. Birkedal, M. Elsman, N. Hallenberg, T.H. Olesen, and P. Sestoft
The IT University of Copenhagen, September 2001. (234 pages).
.pdf
Relative and Modified Relative Realizability
L. Birkedal and J. van Oosten
Annals of Pure and Applied Logic, 118(1–2):115–132, 2002.
.pdf
Elementary Axioms for Local Maps of Toposes
S. Awodey and L. Birkedal
Journal of Pure and Applied Algebra, 177(3):215–230, February 2003.
.pdf
Developing Theories of Types and Computability via Realizability
L. Birkedal
Electronic Notes in Theoretical Computer Science, 34, 2000. (Book version of PhD thesis.)
.pdf
W-Types and M-Types in Equilogical Spaces
A. Bauer and L. Birkedal
Manuscript, 1999.
.pdf
Continuous Functionals of Dependent Types and Equilogical Spaces
A. Bauer and L. Birkedal
In CSL 2000: Computer Science Logic
.pdf
Tutorial Workshop on Realizability Semantics, FLoC'99, Trento
L. Birkedal, J. van Oosten, G. Rosolini, and D.S. Scott, editors.
Mathematical Structures in Computer Science volume 12. Cambridge University Press, 2002
Local Realizability Toposes and a Modal Logic for Computability
S. Awodey, L. Birkedal, and D.S. Scott
Mathematical Structures in Computer Science, 12(3):319–334, 2002.
.pdf
Developing Theories of Types and Computability via Realizability
L. Birkedal
PhD thesis, School of Computer Science, Carnegie Mellon University, December 1999. Available as CMU Technical Report: CMU-CS-99-173
.pdf
A General Notion of Realizability
L. Birkedal
IN LICS 2000: Logic in Computer Science
.pdf
Local Realizability Toposes and a Modal Logic for Computability
S. Awodey, L. Birkedal, and D.S. Scott
In L. Birkedal, J. van Oosten, G. Rosolini, and D.S. Scott, editors, Tutorial Workshop on Realizability Semantics, FLoC'99, Trento, Italy, 1999, volume 23 of Electronic Notes in Theoretical Computer Science. Elsevier, 1999.
.pdf
Equilogical Spaces
A. Bauer, L. Birkedal, and D.S. Scott
Theoretical Computer Science, 315(1):35–59, 2004.
.pdf
Type Theory via Exact Categories
L. Birkedal, A. Carboni, G. Rosolini, and D.S. Scott
In LICS 1998: Logic in Computer Science.
.pdf
Constructing Interpretations of Recursives Types in an Operational Setting
L. Birkedal and R.W. Harper
Information and Computation, 155:3–63, 1999.
.pdf
Constructing Interpretations of Recursive Types in an Operational Setting (Summary)
L. Birkedal and R.W. Harper
In TACS 1997: Theoretical Aspects of Computer Software: International Symposium, Sendai, Japan
.pdf
A Constraint-Based Region Inference Algorithm
L. Birkedal and M. Tofte
Theoretical Computer Science, 258:299–392, 2001.
.pdf
A Region Inference Algorithm
M. Tofte and L. Birkedal
ACM Transactions on Programming Languages and Systems (TOPLAS) 20(4):734–767, July 1998.
.pdf
Unification and Polymorphism in Region Inference
M. Tofte and L. Birkedal
In Milner Festschrift, Cambridge University Press, 1998.
.pdf
From Region Inference to von Neumann Machines via Region Representation Inference
L. Birkedal, M. Tofte, and M. Vejlstrup
In POPL 1996: Principles of Programming Languages.
.pdf
Programming with regions in the ML Kit (for Version 3)
M. Tofte, L. Birkedal, M. Elsman, N. Hallenberg, T.H. Olesen, P. Sestoft, and P. Bertelsen
Technical Report 98/25, Department of Computer Science, University of Copenhagen, November 1998. (214 pages).
.pdf
Programming with regions in the ML Kit
M. Tofte, L. Birkedal, M. Elsman, N. Hallenberg, T.H. Olesen, P. Sestoft, and P. Bertelsen.
Technical Report 97/12, Department of Computer Science, University of Copenhagen, 1997. (194 pages).
.pdf
The ML Kit, Version 1
L. Birkedal, N. Rothwell, M. Tofte, and D.N. Turner
Technical Report 93/14, Department of Computer Science, University of Copenhagen, 1993. (112 pages).
.pdf
Binding-Time Analysis for Standard ML
L. Birkedal and M. Welinder
Lisp and Symbolic Computation, 8(3):191–208, September 1995.
.pdf
Binding-Time Analysis for Standard ML
L. Birkedal and M. Welinder
In PEPM 1994: ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation
.pdf
Handwriting Program Generator Generators
L. Birkedal and M. Welinder
IN PLILP 1994: Programming Language Implementation and Logic Programming
.pdf
Partial evaluation of Standard ML
L. Birkedal and M. Welinder
Technical Report 93/22, DIKU, Department of Computer Science, University of Copenhagen, October 1993. Master's Thesis. (173 pages).
.pdf
Higher-Order Functors and Principal Signatures in Standard ML
L. Birkedal
TOPPS Report D–184 (117 pages), September 1993.
.pdf
Towards a Semantic Foundation for Binding-Time Analysis
L. Birkedal and and N.J. Rehof
DIKU Student Project, April 1993.