Lars Birkedal

ORCID

Publication Activity (10 Years)

Years Active: 1994-2024
Publications (10 Years): 90

Top Venues

Proc. ACM Program. Lang.

CoRR

ESOP

POPL

Publications

Filip Sieczkowski, Sergei Stepanenko, Jonathan Sterling, Lars Birkedal
The Essence of Generalized Algebraic Data Types. Proc. ACM Program. Lang. 8 (POPL) (2024)
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal
Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code. J. ACM 71 (1) (2024)
Amin Timany, Armaël Guéneau, Lars Birkedal
The Logical Essence of Well-Bracketed Control Flow. Proc. ACM Program. Lang. 8 (POPL) (2024)
Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
Tachis: Higher-Order Separation Logic with Credits for Expected Costs. CoRR (2024)
Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
Approximate Relational Reasoning for Higher-Order Probabilistic Programs. CoRR (2024)
Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Jonas Kastberg Hinrichsen, Léon Gondelman, Abel Nieto, Lars Birkedal
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement. Proc. ACM Program. Lang. 8 (POPL) (2024)
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
Almost-Sure Termination by Guarded Refinement. CoRR (2024)
Angus Hammond, Zongyuan Liu, Thibaut Pérami, Peter Sewell, Lars Birkedal, Jean Pichon-Pharabod
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic. Proc. ACM Program. Lang. 8 (POPL) (2024)
Jonathan Sterling, Daniel Gratzer, Lars Birkedal
Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics. CSL (2024)
Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs. CoRR (2024)
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. Proc. ACM Program. Lang. 8 (POPL) (2024)
Dan Frumin, Amin Timany, Lars Birkedal
Modular Denotational Semantics for Effects with Guarded Interaction Trees. Proc. ACM Program. Lang. 8 (POPL) (2024)
Léon Gondelman, Jonas Kastberg Hinrichsen, Mário Pereira, Amin Timany, Lars Birkedal
Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols. Proc. ACM Program. Lang. 7 (ICFP) (2023)
Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, Lars Birkedal
Modular Verification of State-Based CRDTs in Separation Logic (Artifact). Dagstuhl Artifacts Ser. 9 (2) (2023)
Alejandro Aguirre, Lars Birkedal
Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice. Proc. ACM Program. Lang. 7 (POPL) (2023)
Zongyuan Liu, Sergei Stepanenko, Jean Pichon-Pharabod, Amin Timany, Aslan Askarov, Lars Birkedal
VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Xiaojia Rao, Aïna Linn Georges, Maxime Legoupil, Conrad Watt, Jean Pichon-Pharabod, Philippa Gardner, Lars Birkedal
Iris-Wasm: Robust and Modular Verification of WebAssembly Programs. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Simon Friis Vindum, Lars Birkedal
Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory. Proc. ACM Program. Lang. 7 (OOPSLA2) (2023)
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. CoRR (2023)
Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, Lars Birkedal
Modular Verification of State-Based CRDTs in Separation Logic. ECOOP (2023)
Frederik Lerbjerg Aagaard, Jonathan Sterling, Lars Birkedal
A denotationally-based program logic for higher-order store. CoRR (2023)
Dan Frumin, Amin Timany, Lars Birkedal
Modular Denotational Semantics for Effects with Guarded Interaction Trees. CoRR (2023)
Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, Derek Dreyer
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C. Proc. ACM Program. Lang. 7 (OOPSLA2) (2023)
Jonathan Sterling, Daniel Gratzer, Lars Birkedal
Free theorems from univalent reference types. CoRR (2023)
Aïna Linn Georges, Alix Trieu, Lars Birkedal
Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities. Proc. ACM Program. Lang. 6 (OOPSLA) (2022)
Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
Later credits: resourceful reasoning for the later modality. Proc. ACM Program. Lang. 6 (ICFP) (2022)
Jonathan Sterling, Daniel Gratzer, Lars Birkedal
Denotational semantics of general store and polymorphism. CoRR (2022)
Simon Friis Vindum, Dan Frumin, Lars Birkedal
Mechanized verification of a fine-grained concurrent queue from meta's folly library. CPP (2022)
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, Lars Birkedal
Controlling unfolding in type theory. CoRR (2022)
Philipp Stassen, Daniel Gratzer, Lars Birkedal
{mitten}: A Flexible Multimodal Proof Assistant. TYPES (2022)
Daniel Gratzer, Evan Cavallo, G. A. Kavvos, Adrien Guatto, Lars Birkedal
Modalities and Parametric Adjoints. ACM Trans. Comput. Log. 23 (3) (2022)
Daniel Gratzer, Lars Birkedal
A Stratified Approach to Löb Induction. FSCD (2022)
Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, Lars Birkedal
Modular verification of op-based CRDTs in separation logic. Proc. ACM Program. Lang. 6 (OOPSLA2) (2022)
Thomas Van Strydonck, Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, Dominique Devriese
Proving full-system security properties under multiple attacker models on capability machines. CSF (2022)
Frederik Lerbjerg Aagaard, Magnus Baunsgaard Kristensen, Daniel Gratzer, Lars Birkedal
Unifying cubical and multimodal type theory. CoRR (2022)
Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal
Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. PLDI (2021)
Zesen Qian, G. A. Kavvos, Lars Birkedal
Client-server sessions in linear logic. Proc. ACM Program. Lang. 5 (ICFP) (2021)
Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Léon Gondelman, Abel Nieto, Lars Birkedal
Trillium: Unifying Refinement and Higher-Order Distributed Separation Logic. CoRR (2021)
Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, Lars Birkedal
Distributed causal memory: modular specification and verification in higher-order distributed separation logic. Proc. ACM Program. Lang. 5 (POPL) (2021)
Dan Frumin, Robbert Krebbers, Lars Birkedal
Compositional Non-Interference for Fine-Grained Concurrent Programs. IEEE Symposium on Security and Privacy (2021)
Simon Friis Vindum, Lars Birkedal
Contextual refinement of the Michael-Scott queue (proof pearl). CPP (2021)
Simon Oddershede Gregersen, Johan Bay, Amin Timany, Lars Birkedal
Mechanized logical relations for termination-insensitive noninterference. Proc. ACM Program. Lang. 5 (POPL) (2021)
Dan Frumin, Robbert Krebbers, Lars Birkedal
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. Log. Methods Comput. Sci. 17 (3) (2021)
Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, Nikos Tzevelekos
Theorems for free from separation logic specifications. Proc. ACM Program. Lang. 5 (ICFP) (2021)
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, Lars Birkedal
Efficient and provable local capability revocation using uninitialized capabilities. Proc. ACM Program. Lang. 5 (POPL) (2021)
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities. J. Funct. Program. 31 (2021)
Amin Timany, Lars Birkedal
Reasoning about monotonicity in separation logic. CPP (2021)
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal
Multimodal Dependent Type Theory. Log. Methods Comput. Sci. 17 (3) (2021)
Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, Bas Spitters
Modal dependent type theory and dependent right adjoints. Math. Struct. Comput. Sci. 30 (2) (2020)
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal
Multimodal Dependent Type Theory. LICS (2020)
Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, Lars Birkedal
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. ESOP (2020)
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
Reasoning about a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management. ACM Trans. Program. Lang. Syst. 42 (1) (2020)
Dan Frumin, Robbert Krebbers, Lars Birkedal
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. CoRR (2020)
Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, Robbert Krebbers
Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris. Proc. ACM Program. Lang. 4 (ICFP) (2020)
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal
Multimodal Dependent Type Theory. CoRR (2020)
Zesen Qian, G. A. Kavvos, Lars Birkedal
Client-Server Sessions in Linear Logic. CoRR (2020)
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities. Proc. ACM Program. Lang. 3 (POPL) (2019)
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi
Guarded Cubical Type Theory. J. Autom. Reason. 63 (2) (2019)
Dan Frumin, Robbert Krebbers, Lars Birkedal
Compositional Non-Interference for Fine-Grained Concurrent Programs. CoRR (2019)
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
Reasoning About a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management - Technical Appendix Including Proofs and Details. CoRR (2019)
Daniel Gratzer, Jonathan Sterling, Lars Birkedal
Implementing a modal dependent type theory. Proc. ACM Program. Lang. 3 (ICFP) (2019)
Ales Bizjak, Daniel Gratzer, Robbert Krebbers, Lars Birkedal
Iron: managing obligations in higher-order concurrent separation logic. Proc. ACM Program. Lang. 3 (POPL) (2019)
Amin Timany, Lars Birkedal
Mechanized relational verification of concurrent programs with continuations. Proc. ACM Program. Lang. 3 (ICFP) (2019)
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, Derek Dreyer
Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018)
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
Reasoning About a Machine with Local Capabilities - Provably Safe Stack and Return Pointer Management. ESOP (2018)
Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, Lars Birkedal
A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST. Proc. ACM Program. Lang. 2 (POPL) (2018)
Dan Frumin, Robbert Krebbers, Lars Birkedal
ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. LICS (2018)
Ales Bizjak, Lars Birkedal
A model of guarded recursion via generalised equilogical spaces. Theor. Comput. Sci. 722 (2018)
Ales Bizjak, Lars Birkedal
On Models of Higher-Order Separation Logic. MFPS (2018)
Aleksandr Karbyshev, Kasper Svendsen, Aslan Askarov, Lars Birkedal
Compositional Non-interference for Concurrent Programs via Separation and Framing. POST (2018)
Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. CoRR (2018)
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
StkTokens: Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities - Technical Report with Proofs and Details. CoRR (2018)
Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. ESOP (2018)
Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal
The Essence of Higher-Order Concurrent Separation Logic. ESOP (2017)
Morten Krogh-Jespersen, Kasper Svendsen, Lars Birkedal
A relational model of types-and-effects in higher-order concurrent separation logic. POPL (2017)
Robbert Krebbers, Amin Timany, Lars Birkedal
Interactive proofs in higher-order concurrent separation logic. POPL (2017)
Lars Birkedal, Thomas Dinsdale-Young, Guilhem Jaber, Kasper Svendsen, Nikos Tzevelekos
Trace Properties from Separation Logic Specifications. CoRR (2017)
Thomas Dinsdale-Young, Pedro da Rocha Pinto, Kristoffer Just Andersen, Lars Birkedal
Caper - Automatic Verification for Fine-Grained Concurrency. ESOP (2017)
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi
Guarded Cubical Type Theory: Path Equality for Guarded Recursion. CSL (2016)
Ales Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus Ejlers Møgelberg, Lars Birkedal
Guarded Dependent Type Theory with Coinductive Types. CoRR (2016)
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi
Guarded Cubical Type Theory: Path Equality for Guarded Recursion. CoRR (2016)
Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
Higher-order ghost state. ICFP (2016)
Dominique Devriese, Lars Birkedal, Frank Piessens
Reasoning about Object Capabilities with Logical Relations and Effect Parametricity. EuroS&P (2016)
Ranald Clouston, Ales Bizjak, Hans Bugge Grathwohl, Lars Birkedal
The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. Log. Methods Comput. Sci. 12 (3) (2016)
Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson, Kasper Svendsen, Lars Birkedal
Verifying Custom Synchronization Constructs Using Higher-Order Separation Logic. ACM Trans. Program. Lang. Syst. 38 (2) (2016)
Lars Birkedal, Guilhem Jaber, Filip Sieczkowski, Jacob Thamsborg
A Kripke logical relation for effect-based program transformations. Inf. Comput. 249 (2016)
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi
Guarded Cubical Type Theory. CoRR (2016)
Kasper Svendsen, Filip Sieczkowski, Lars Birkedal
Transfinite Step-Indexing: Decoupling Concrete and Logical Steps. ESOP (2016)
Ales Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus Ejlers Møgelberg, Lars Birkedal
Guarded Dependent Type Theory with Coinductive Types. FoSSaCS (2016)
Lars Birkedal
Preface. MFPS (2016)
Filip Sieczkowski, Ales Bizjak, Lars Birkedal
ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages. ITP (2015)
Marco Paviotti, Rasmus Ejlers Møgelberg, Lars Birkedal
A Model of PCF in Guarded Type Theory. MFPS (2015)
Lars Birkedal, Derek Dreyer, Philippa Gardner, Zhong Shao
Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191). Dagstuhl Reports 5 (5) (2015)
Ales Bizjak, Lars Birkedal
Step-Indexed Logical Relations for Probability. FoSSaCS (2015)
Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. POPL (2015)
Ranald Clouston, Ales Bizjak, Hans Bugge Grathwohl, Lars Birkedal
Programming and Reasoning with Guarded Recursion for Coinductive Types. FoSSaCS (2015)
Ales Bizjak, Lars Birkedal
Step-Indexed Logical Relations for Probability (long version). CoRR (2015)
Ranald Clouston, Ales Bizjak, Hans Bugge Grathwohl, Lars Birkedal
Programming and Reasoning with Guarded Recursion for Coinductive Types. CoRR (2015)
Filip Sieczkowski, Kasper Svendsen, Lars Birkedal, Jean Pichon-Pharabod
A Separation Logic for Fictional Sequential Consistency. ESOP (2015)
Ales Bizjak, Lars Birkedal, Marino Miculan
A Model of Countable Nondeterminism in Guarded Type Theory. RTA-TLCA (2014)

Lars Birkedal.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Lars Birkedal