Publications of Lars Birkedal

Google Scholar entry DBLP entry

Chronological Listing (BibTeX database: BirkedalL.bib)

A Logical Approach to Type Soundness
A. Timany, R. Krebbers, D. Dreyer, and L. Birkedal.
Submitted for publication.
Controlling unfolding in type theory
D. Gratzer, J. Sterling, C. Angiuli, T. Coquand, and L. Birkedal
Submitted for publication.
Denotational semantics of general store and polymorphism
J. Sterling, D. Gratzer, and L. Birkedal
Submitted for publication.
Unifying Cubical and Multimodal Type Theory
F.L. Aagaard, M.B. Kristensen, D. Gratzer, and L. Birkedal.
Submitted for publication.
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
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.
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.
The Essence of Generalized Algebraic Data Types
F. Sieczkowski, S. Stepanenko, J. Sterling, and L. Birkedal.
In Proceedings of POPL 2024.
The Logical Essence of Well-Bracketed Control Flow
A. Timany, A. Gueneau, and L. Birkedal.
In Proceedings of POPL 2024.
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.
Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics
J. Sterling, D. Gratzer, and L. Birkedal.
In Proceedings of CSL 2024.
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.
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
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.
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.
mitten: A Flexible Multimodal Proof Assistant
P. Stassen, D. Gratzer, and L. Birkedal
In Proceedings of Types 2022 (LIPIcs, Volume 269, TYPES 2022).
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.
A denotationally-based program logic for higher-order store.
F.L. Aagaard, J. Sterling, and L. Birkedal
In Proceedings of MFPS 2023.
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
S.O. Gregersen, A. Aguirre, P. Haselwarter, J. Tassarotti, and L. Birkedal.
arXiv:2301.10061
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.
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.
Step-Indexed Logical Relations for Nondeterministic and Probabilistic Choice
A. Aguirre and L. Birkedal
In Proceedings of POPL 2023.
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.
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
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.
A Stratified Approach to Loeb Induction
D. Gratzer and L. Birkedal
In Proceedings of FSCD 2022.
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.
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.
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
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
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
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.
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
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.
Contextual Refinement of the Michael-Scott Queue (Proof Pearl)
S.F. Vindum and L. Birkedal
In CPP 2021: Certified Proofs and Programs.
Reasoning About Monotonicity in Separation Logic
A. Timany and L. Birkedal
In CPP 2021: Certified Proofs and Programs.
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.
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.
Mechanized Logical Relations for Termination-Insensitive Noninterference
S.O. Gregersen, J. Bay, A. Timany, and L. Birkedal
In POPL 2021: Principles of Programming Languages.
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.
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.
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
Compositional Non-Interference for Fine-Grained Concurrent Programs
D. Frumin, R. Krebbers, and L. Birkedal
In S&P 2021: Security and Privacy (Oakland)
Multimodal Dependent Type Theory
D. Gratzer, G. A. Kavvos, A. Nuyts, and L. Birkedal
In LICS 2020: Logic in Computer Science
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
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
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
Mechanized Relational Verification of Concurrent Programs with Continuations
A. Timany and L. Birkedal
In ICFP 2019: International Conference on Functional Programming, Berlin, Germany
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
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
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
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
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
ReLoC: a Mechanised Relational Logic for Fine-Grained Concurrency
D. Frumin, R. Krebbers, and L. Birkedal
In LICS 2018: Logic in Computer Science
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
A Model of Guarded Recursion via Generalised Equilogical Spaces
A. Bizjak and L. Birkedal
Theoretical Computer Science, 772:1–18, 2018
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
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
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
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
On Models of Higher-Order Separation Logic
A. Bizjak and L. Birkedal
In MFPS 2017: Mathematical Foundations of Programming Semantics
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
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
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
Interactive Proofs in Higher-Order Concurrent Separation Logic
R. Krebbers, A. Timany, and L. Birkedal
In POPL 2017: Principles of Programming Languages
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
Higher-Order Ghost State
R. Jung, R. Krebbers, L. Birkedal, and D. Dreyer.
In ICFP 2016: International Conference on Functional Programming
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
A Kripke Logical Relation for Effect-Based Program Transformations
L. Birkedal, G. Jaber, F. Sieczkowski, and J. Thamsborg
Information and Computation, 2016
Guarded Cubical Type Theory
L. Birkedal, A. Bizjak, R. Clouston, H.B. Gratwohl, B. Spitters, and A. Vezzosi.
In TYPES 2016
Transfinite Step-Indexing: Decoupling Concrete and Logical Steps
K. Svendsen, F. Sieczkowski, and L. Birkedal
In ESOP 2016: European Symposium on Programming
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
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
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
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
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
Step-indexed Logical Relations for Probability
A. Bizjak, and L. Birkedal
In FOSSACS 2015: Foundations of Software Science and Computation Structures
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
A Separation Logic for Fictional Sequential Consistency
F. Sieczkowski, K. Svendsen, L. Birkedal, and J. Pichon-Pharapod
In ESOP 2015: European Symposium on Programming
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
A Model of Countable Nondeterminism in Guarded Type Theory
A. Bizjak, L. Birkedal, and M. Miculan
In TLCA 2014: Typed Lambda Calculus and Applications
Impredicative Concurrent Abstract Predicates
K. Svendsen and L. Birkedal
In ESOP 2014: European Symposium on Programming
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.
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
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
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
Modular Reasoning about Separation of Concurrent Data Structures
K. Svendsen, L. Birkedal, and M. Parkinson
In ESOP 2013: European Symposium on Programming
A Note on the Transitivity of Step-Indexed Logical Relations
Lars Birkedal and Ales Bizjak
Manuscript, 2012
Logical Relations for Fine-Grained Concurrency
A. Turon, J. Thamsborg, A. Ahmed, L. Birkedal, and D. Dreyer
In POPL 2013: Principles of Programming Languages
Views: Compositional Reasoning for Concurrency
T. Dinsdale-Young, L. Birkedal, P. Gardner, M. Parkinson, and H. Yang
In POPL 2013: Principles of Programming Languages
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.
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.
A Concurrent Logical Relation
L. Birkedal, F. Sieczkowski, and J. Thamsborg
In CSL 2012: Computer Science Logic
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
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,
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.
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.
Fictional Separation Logic
J.B. Jensen and L. Birkedal
In ESOP 2012: European Symposium on Programming
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
An Inductive Characterization of Matching in Binding Bigraphs
T.C. Damgaard, A.J. Glenstrup, L. Birkedal, and R. Milner
Formal Aspects of Computing 2012
Step-Indexed Relational Reasoning for Countable Nondeterminism
J. Schwinghammer and L. Birkedal
In CSL 2011: Computer Science Logic
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
A Kripke Logical Relation for Effect-Based Program Transformations
J. Thamsborg and L. Birkedal
In ICFP 2011: International Conference on Functional Programming
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.
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
Partiality, State, and Dependent Types
K. Svendsen, L. Birkedal, and A. Nanevski
In TLCA 2011: Typed Lambda Calculus and Applications
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
Logical Step-Indexed Logical Relations
D. Dreyer, A. Ahmed, and L. Birkedal
Logical Methods in Computer Science, 7(2:16), June 2011.
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
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
The Category-Theoretic Solution of Recursive Metric-Space Equations
L. Birkedal, K. Støvring, and J. Thamsborg
Theoretical Computer Science, 411:4102–4122, 2010.
Formalizing Domains, Ultrametric Spaces and Semantics of Programming Languages
N. Benton, L. Birkedal, A. Kennedy, and C. Varming
Manuscript, 2010.
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
A Metric Model of Guarded Recursion
L. Birkedal, J. Schwinghammer, and K. Støvring
In FICS 2012: Fixed Points in Computer Science
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.
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
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
Verifying Generics and Delegates
K. Svendsen, L. Birkedal, and M. Parkinson
In ECOOP 2010: European Conference on Object-Oriented Programming
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.
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
Verifying Event-Driven Programs using Ramified Frame Properties
N. Krishnaswami, L. Birkedal, and J. Aldrich
In TLDI 2010: Types in Language Design and Implementation
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.
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
Solutions of Generalized Recursive Metric-Space Equations
L. Birkedal, K. Støvring, and J. Thamsborg
In FICS 2009: Fixed Points in Computer Science
Logical Step-Indexed Logical Relations
D. Dreyer, A. Ahmed, and L. Birkedal
In LICS 2009: Logic in Computer Science
Nested Hoare Triples and Frame Rules for Higher-Order Store
In CSL 2009: Computer Science Logic
place
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.
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
Relational Parametricity for References and Recursive Types
L. Birkedal, K. Støvring, and J. Thamsborg
In TLDI 2009: Types in Language Design and Implementation
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
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.
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
On the Construction of Sorted Bigraphical Reactive Systems
L. Birkedal, S. Debois, and T. Hildebrandt
In CONCUR 2008: International Conference on Concurrency
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.
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.
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
Higher-Order Separation Logic in Isabelle/HOLCF
C. Varming and L. Birkedal
In MFPS 2008: Mathematical Foundations of Programming Semantics
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
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.
An Implementation of Bigraph Matching
A.J. Glenstrup, T.C. Damgaard, L. Birkedal, and E. Højsgaard
Manuscript, 2007
Hoare Type Theory, Polymorphism and Separation
A. Nanevski, G. Morrisett, and L. Birkedal
Journal of Functional Programming, 2007.
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
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.
Matching of Bigraphs
L. Birkedal, T.C. Damgaard, A. Glenstrup, and R. Milner
In Graph Transformation for Verification and Concurrency 2006
Relational Parametricity and Separation Logic
L. Birkedal and H. Yang
In FOSSACS 2007: Foundations of Software Science and Computation Structures
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
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.
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.
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.
Polymorphism and Separation in Hoare Type Theory
A. Nanevski, G. Morrisett, and L. Birkedal
In ICFP 2006: International Conference on Functional Programming
Sortings for Reactive Systems
L. Birkedal, S. Debois, and T. Hildebrandt
In CONCUR 2006: International Conference on Concurrency Theory
Relational Reasoning for Recursive Types and References
N. Bohr and L. Birkedal
In APLAS 2006: Asian Symposium on Programming Languages and Systems
Operational Semantics and Models of Linear Abadi & Plotkin Logic
L. Birkedal, R.L. Petersen, R. Møgelberg, and C. Varming
Manuscript, 2006
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.
Axiomatizing Binding Bigraphs
T.C. Damgaard and L. Birkedal
Nordic Journal of Computing, 13(1-2):58–77, 2006.
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.
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
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
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.
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
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
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.
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.
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.
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
BI-Hyperdoctrines and Higher-Order Separation Logic
B. Biering, L. Birkedal, and N. Torp-Smith
In ESOP 2005: European Symposium on Programming
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.
Bigraphical Programming Languages - a LaCoMoCo Research Project
L. Birkedal
In 2nd UK-Ubinet Workshop, Cambridge, UK, May 2004. Position Paper.
On the Definition of Parametricity
L. Birkedal and R.E. Møgelberg
Technical Report 44, The IT University of Copenhagen, 2004.
A Retrospective on Region-Based Memory Management
M. Tofte, L. Birkedal, M. Elsman, and N. Hallenberg
Higher Order Symbolic Computation, 17(2), 2004.
Local Reasoning about a Copying Garbage Collector
L. Birkedal, N. Torp-Smith, and J.C. Reynolds
In POPL 2004: Principles of Programming Languages
A General Notion of Realizability
L. Birkedal
Bulletin of Symbolic Logic, 8(2):266–282, 2002.
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).
Relative and Modified Relative Realizability
L. Birkedal and J. van Oosten
Annals of Pure and Applied Logic, 118(1–2):115–132, 2002.
Elementary Axioms for Local Maps of Toposes
S. Awodey and L. Birkedal
Journal of Pure and Applied Algebra, 177(3):215–230, February 2003.
Developing Theories of Types and Computability via Realizability
L. Birkedal
Electronic Notes in Theoretical Computer Science, 34, 2000. (Book version of PhD thesis.)
W-Types and M-Types in Equilogical Spaces
A. Bauer and L. Birkedal
Manuscript, 1999.
Continuous Functionals of Dependent Types and Equilogical Spaces
A. Bauer and L. Birkedal
In CSL 2000: Computer Science Logic
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.
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
A General Notion of Realizability
L. Birkedal
IN LICS 2000: Logic in Computer Science
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.
Equilogical Spaces
A. Bauer, L. Birkedal, and D.S. Scott
Theoretical Computer Science, 315(1):35–59, 2004.
Type Theory via Exact Categories
L. Birkedal, A. Carboni, G. Rosolini, and D.S. Scott
In LICS 1998: Logic in Computer Science.
Constructing Interpretations of Recursives Types in an Operational Setting
L. Birkedal and R.W. Harper
Information and Computation, 155:3–63, 1999.
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
A Constraint-Based Region Inference Algorithm
L. Birkedal and M. Tofte
Theoretical Computer Science, 258:299–392, 2001.
A Region Inference Algorithm
M. Tofte and L. Birkedal
ACM Transactions on Programming Languages and Systems (TOPLAS) 20(4):734–767, July 1998.
Unification and Polymorphism in Region Inference
M. Tofte and L. Birkedal
In Milner Festschrift, Cambridge University Press, 1998.
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.
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).
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).
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).
Binding-Time Analysis for Standard ML
L. Birkedal and M. Welinder
Lisp and Symbolic Computation, 8(3):191–208, September 1995.
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
Handwriting Program Generator Generators
L. Birkedal and M. Welinder
IN PLILP 1994: Programming Language Implementation and Logic Programming
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).
Higher-Order Functors and Principal Signatures in Standard ML
L. Birkedal
TOPPS Report D–184 (117 pages), September 1993.
Towards a Semantic Foundation for Binding-Time Analysis
L. Birkedal and and N.J. Rehof
DIKU Student Project, April 1993.