Lars Birkedal

231 papers A* 20A 24B 38C 2Journal 118Unranked 25
YearRankTypeTitle / Venue / Authors
2026 J jnl
An Axiomatic Basis for Computer Programming on Relaxed Hardware Architectures: The AxSL Logics.
ACM Trans. Program. Lang. Syst.
Zongyuan Liu, Angus Hammond, Thibaut Pérami, Peter Sewell, Lars Birkedal, Jean Pichon-Pharabod
2026 B conf
Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic.
CPP
Virgil Marionneau, Félix Sassus Bourda, Alejandro Aguirre, Lars Birkedal
2025 J jnl
Approximate Relational Reasoning for Higher-Order Probabilistic Programs.
Proc. ACM Program. Lang.
Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
2025 J jnl
Context-Dependent Effects and Concurrency in Guarded Interaction Trees.
CoRR
Sergei Stepanenko, Emma Nardino, Virgil Marionneau, Dan Frumin, Amin Timany, Lars Birkedal
2025 — conf
Context-Dependent Effects in Guarded Interaction Trees.
ESOP (2)
Sergei Stepanenko, Emma Nardino, Dan Frumin, Amin Timany, Lars Birkedal
2025 J jnl
Contextual Refinement of Higher-Order Concurrent Probabilistic Programs.
CoRR
Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
2025 J jnl
Controlling unfolding in type theory.
Math. Struct. Comput. Sci.
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, Lars Birkedal
2025 B conf
Idempotent Resources in Separation Logic - The Heart of core in Iris.
FoSSaCS
Daniel Gratzer, Mathias Adam Møller, Lars Birkedal
2025 J jnl
Modelling Recursion and Probabilistic Choice in Guarded Type Theory.
Proc. ACM Program. Lang.
Philipp Stassen, Rasmus Ejlers Møgelberg, Maaike Zwart, Alejandro Aguirre, Lars Birkedal
2025 J jnl
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs.
CoRR
Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
2025 J jnl
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs.
Proc. ACM Program. Lang.
Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
2025 J jnl
Reasoning about Weak Isolation Levels in Separation Logic.
CoRR
Anders Alnor Mathiasen, Léon Gondelman, Léon Ducruet, Amin Timany, Lars Birkedal
2025 J jnl
Reasoning about Weak Isolation Levels in Separation Logic.
Proc. ACM Program. Lang.
Anders Alnor Mathiasen, Léon Gondelman, Léon Ducruet, Amin Timany, Lars Birkedal
2025 B conf
The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic.
CPP
Simon Friis Vindum, Aïna Linn Georges, Lars Birkedal
2024 J jnl
A Logical Approach to Type Soundness.
J. ACM
Amin Timany, Robbert Krebbers, Derek Dreyer, Lars Birkedal
2024 J jnl
Almost-Sure Termination by Guarded Refinement.
CoRR
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Almost-Sure Termination by Guarded Refinement.
Proc. ACM Program. Lang.
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
2024 J jnl
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic.
Proc. ACM Program. Lang.
Angus Hammond, Zongyuan Liu, Thibaut Pérami, Peter Sewell, Lars Birkedal, Jean Pichon-Pharabod
2024 J jnl
Approximate Relational Reasoning for Higher-Order Probabilistic Programs.
CoRR
Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic.
Proc. ACM Program. Lang.
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code.
J. ACM
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal
2024 J jnl
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs.
CoRR
Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs.
Proc. ACM Program. Lang.
Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly.
Proc. ACM Program. Lang.
Maxime Legoupil, June Rousseau, Aïna Linn Georges, Jean Pichon-Pharabod, Lars Birkedal
2024 J jnl
Modelling Probabilistic FPC in Guarded Type Theory.
CoRR
Philipp Stassen, Rasmus Ejlers Møgelberg, Maaike Zwart, Alejandro Aguirre, Lars Birkedal
2024 J jnl
Modular Denotational Semantics for Effects with Guarded Interaction Trees.
Proc. ACM Program. Lang.
Dan Frumin, Amin Timany, Lars Birkedal
2024 J jnl
Tachis: Higher-Order Separation Logic with Credits for Expected Costs.
CoRR
Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
2024 J jnl
Tachis: Higher-Order Separation Logic with Credits for Expected Costs.
Proc. ACM Program. Lang.
Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
2024 J jnl
The Essence of Generalized Algebraic Data Types.
Proc. ACM Program. Lang.
Filip Sieczkowski, Sergei Stepanenko, Jonathan Sterling, Lars Birkedal
2024 J jnl
The Logical Essence of Well-Bracketed Control Flow.
Proc. ACM Program. Lang.
Amin Timany, Armaël Guéneau, Lars Birkedal
2024 B conf
Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics.
CSL
Jonathan Sterling, Daniel Gratzer, Lars Birkedal
2024 J jnl
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement.
Proc. ACM Program. Lang.
Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Jonas Kastberg Hinrichsen, Léon Gondelman, Abel Nieto, Lars Birkedal
2024 J jnl
Unifying cubical and multimodal type theory.
Log. Methods Comput. Sci.
Frederik Lerbjerg Aagaard, Magnus Baunsgaard Kristensen, Daniel Gratzer, Lars Birkedal
2023 B conf
A denotationally-based program logic for higher-order store.
MFPS
Frederik Lerbjerg Aagaard, Jonathan Sterling, Lars Birkedal
2023 J jnl
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic.
CoRR
Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal
2023 J jnl
Free theorems from univalent reference types.
CoRR
Jonathan Sterling, Daniel Gratzer, Lars Birkedal
2023 J jnl
Iris-Wasm: Robust and Modular Verification of WebAssembly Programs.
Proc. ACM Program. Lang.
Xiaojia Rao, Aïna Linn Georges, Maxime Legoupil, Conrad Watt, Jean Pichon-Pharabod, Philippa Gardner, Lars Birkedal
2023 J jnl
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C.
Proc. ACM Program. Lang.
Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, Derek Dreyer
2023 J jnl
Modular Denotational Semantics for Effects with Guarded Interaction Trees.
CoRR
Dan Frumin, Amin Timany, Lars Birkedal
2023 J jnl
Modular Verification of State-Based CRDTs in Separation Logic (Artifact).
Dagstuhl Artifacts Ser.
Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, Lars Birkedal
2023 A conf
Modular Verification of State-Based CRDTs in Separation Logic.
ECOOP
Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, Lars Birkedal
2023 J jnl
Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory.
Proc. ACM Program. Lang.
Simon Friis Vindum, Lars Birkedal
2023 J jnl
Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice.
Proc. ACM Program. Lang.
Alejandro Aguirre, Lars Birkedal
2023 J jnl
VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A.
Proc. ACM Program. Lang.
Zongyuan Liu, Sergei Stepanenko, Jean Pichon-Pharabod, Amin Timany, Aslan Askarov, Lars Birkedal
2023 J jnl
Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols.
Proc. ACM Program. Lang.
Léon Gondelman, Jonas Kastberg Hinrichsen, Mário Pereira, Amin Timany, Lars Birkedal
2022 B conf
A Stratified Approach to Löb Induction.
FSCD
Daniel Gratzer, Lars Birkedal
2022 J jnl
Controlling unfolding in type theory.
CoRR
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, Lars Birkedal
2022 J jnl
Denotational semantics of general store and polymorphism.
CoRR
Jonathan Sterling, Daniel Gratzer, Lars Birkedal
2022 J jnl
Later credits: resourceful reasoning for the later modality.
Proc. ACM Program. Lang.
Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
2022 J jnl
Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities.
Proc. ACM Program. Lang.
Aïna Linn Georges, Alix Trieu, Lars Birkedal
2022 B conf
Mechanized verification of a fine-grained concurrent queue from meta's folly library.
CPP
Simon Friis Vindum, Dan Frumin, Lars Birkedal
2022 J jnl
Modalities and Parametric Adjoints.
ACM Trans. Comput. Log.
Daniel Gratzer, Evan Cavallo, G. A. Kavvos, Adrien Guatto, Lars Birkedal
2022 J jnl
Modular verification of op-based CRDTs in separation logic.
Proc. ACM Program. Lang.
Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, Lars Birkedal
2022 A conf
Proving full-system security properties under multiple attacker models on capability machines.
CSF
Thomas Van Strydonck, Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, Dominique Devriese
2022 J jnl
Unifying cubical and multimodal type theory.
CoRR
Frederik Lerbjerg Aagaard, Magnus Baunsgaard Kristensen, Daniel Gratzer, Lars Birkedal
2022 — conf
{mitten}: A Flexible Multimodal Proof Assistant.
TYPES
Philipp Stassen, Daniel Gratzer, Lars Birkedal
2021 J jnl
Client-server sessions in linear logic.
Proc. ACM Program. Lang.
Zesen Qian, G. A. Kavvos, Lars Birkedal
2021 A* conf
Compositional Non-Interference for Fine-Grained Concurrent Programs.
SP
Dan Frumin, Robbert Krebbers, Lars Birkedal
2021 B conf
Contextual refinement of the Michael-Scott queue (proof pearl).
CPP
Simon Friis Vindum, Lars Birkedal
2021 J jnl
Distributed causal memory: modular specification and verification in higher-order distributed separation logic.
Proc. ACM Program. Lang.
Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, Lars Birkedal
2021 J jnl
Efficient and provable local capability revocation using uninitialized capabilities.
Proc. ACM Program. Lang.
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, Lars Birkedal
2021 J jnl
Mechanized logical relations for termination-insensitive noninterference.
Proc. ACM Program. Lang.
Simon Oddershede Gregersen, Johan Bay, Amin Timany, Lars Birkedal
2021 J jnl
Multimodal Dependent Type Theory.
Log. Methods Comput. Sci.
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal
2021 J jnl
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity.
Log. Methods Comput. Sci.
Dan Frumin, Robbert Krebbers, Lars Birkedal
2021 B conf
Reasoning about monotonicity in separation logic.
CPP
Amin Timany, Lars Birkedal
2021 J jnl
StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities.
J. Funct. Program.
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
2021 J jnl
Theorems for free from separation logic specifications.
Proc. ACM Program. Lang.
Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, Nikos Tzevelekos
2021 A* conf
Transfinite Iris: resolving an existential dilemma of step-indexed separation logic.
PLDI
Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal
2021 J jnl
Trillium: Unifying Refinement and Higher-Order Distributed Separation Logic.
CoRR
Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Léon Gondelman, Abel Nieto, Lars Birkedal
2020 A conf
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems.
ESOP
Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, Lars Birkedal
2020 J jnl
Client-Server Sessions in Linear Logic.
CoRR
Zesen Qian, G. A. Kavvos, Lars Birkedal
2020 J jnl
Modal dependent type theory and dependent right adjoints.
Math. Struct. Comput. Sci.
Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, Bas Spitters
2020 A* conf
Multimodal Dependent Type Theory.
LICS
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal
2020 J jnl
Multimodal Dependent Type Theory.
CoRR
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal
2020 J jnl
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity.
CoRR
Dan Frumin, Robbert Krebbers, Lars Birkedal
2020 J jnl
Reasoning about a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management.
ACM Trans. Program. Lang. Syst.
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
2020 J jnl
Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris.
Proc. ACM Program. Lang.
Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, Robbert Krebbers
2019 J jnl
Compositional Non-Interference for Fine-Grained Concurrent Programs.
CoRR
Dan Frumin, Robbert Krebbers, Lars Birkedal
2019 J jnl
Guarded Cubical Type Theory.
J. Autom. Reason.
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi
2019 J jnl
Implementing a modal dependent type theory.
Proc. ACM Program. Lang.
Daniel Gratzer, Jonathan Sterling, Lars Birkedal
2019 J jnl
Iron: managing obligations in higher-order concurrent separation logic.
Proc. ACM Program. Lang.
Ales Bizjak, Daniel Gratzer, Robbert Krebbers, Lars Birkedal
2019 J jnl
Mechanized relational verification of concurrent programs with continuations.
Proc. ACM Program. Lang.
Amin Timany, Lars Birkedal
2019 J jnl
Reasoning About a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management - Technical Appendix Including Proofs and Details.
CoRR
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
2019 J jnl
StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities.
Proc. ACM Program. Lang.
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
2018 J jnl
A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST.
Proc. ACM Program. Lang.
Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, Lars Birkedal
2018 J jnl
A model of guarded recursion via generalised equilogical spaces.
Theor. Comput. Sci.
Ales Bizjak, Lars Birkedal
2018 — conf
Compositional Non-interference for Concurrent Programs via Separation and Framing.
POST
Aleksandr Karbyshev, Kasper Svendsen, Aslan Askarov, Lars Birkedal
2018 J jnl
Iris from the ground up: A modular foundation for higher-order concurrent separation logic.
J. Funct. Program.
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, Derek Dreyer
2018 B conf
On Models of Higher-Order Separation Logic.
MFPS
Ales Bizjak, Lars Birkedal
2018 A* conf
ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency.
LICS
Dan Frumin, Robbert Krebbers, Lars Birkedal
2018 A conf
Reasoning About a Machine with Local Capabilities - Provably Safe Stack and Return Pointer Management.
ESOP
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
2018 A conf
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus.
ESOP
Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg
2018 J jnl
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus.
CoRR
Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg
2018 J jnl
StkTokens: Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities - Technical Report with Proofs and Details.
CoRR
Lau Skorstengaard, Dominique Devriese, Lars Birkedal
2017 A* conf
A relational model of types-and-effects in higher-order concurrent separation logic.
POPL
Morten Krogh-Jespersen, Kasper Svendsen, Lars Birkedal
2017 A conf
Caper - Automatic Verification for Fine-Grained Concurrency.
ESOP
Thomas Dinsdale-Young, Pedro da Rocha Pinto, Kristoffer Just Andersen, Lars Birkedal
2017 A* conf
Interactive proofs in higher-order concurrent separation logic.
POPL
Robbert Krebbers, Amin Timany, Lars Birkedal
2017 A conf
The Essence of Higher-Order Concurrent Separation Logic.
ESOP
Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal
2017 J jnl
Trace Properties from Separation Logic Specifications.
CoRR
Lars Birkedal, Thomas Dinsdale-Young, Guilhem Jaber, Kasper Svendsen, Nikos Tzevelekos
2016 J jnl
A Kripke logical relation for effect-based program transformations.
Inf. Comput.
Lars Birkedal, Guilhem Jaber, Filip Sieczkowski, Jacob Thamsborg
2016 J jnl
Guarded Cubical Type Theory.
CoRR
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi
2016 B conf
Guarded Cubical Type Theory: Path Equality for Guarded Recursion.
CSL
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi
2016 J jnl
Guarded Cubical Type Theory: Path Equality for Guarded Recursion.
CoRR
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi
2016 B conf
Guarded Dependent Type Theory with Coinductive Types.
FoSSaCS
Ales Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus Ejlers Møgelberg, Lars Birkedal
2016 J jnl
Guarded Dependent Type Theory with Coinductive Types.
CoRR
Ales Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus Ejlers Møgelberg, Lars Birkedal
2016 A conf
Higher-order ghost state.
ICFP
Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
2016 B conf
Preface.
MFPS
Lars Birkedal
2016 A conf
Reasoning about Object Capabilities with Logical Relations and Effect Parametricity.
EuroS&P
Dominique Devriese, Lars Birkedal, Frank Piessens
2016 J jnl
The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types.
Log. Methods Comput. Sci.
Ranald Clouston, Ales Bizjak, Hans Bugge Grathwohl, Lars Birkedal
2016 B ed.
The Thirty-second Conference on the Mathematical Foundations of Programming Semantics, MFPS 2016, Carnegie Mellon University, Pittsburgh, PA, USA, May 23-26, 2016
MFPS
Lars Birkedal
2016 A conf
Transfinite Step-Indexing: Decoupling Concrete and Logical Steps.
ESOP
Kasper Svendsen, Filip Sieczkowski, Lars Birkedal
2016 J jnl
Verifying Custom Synchronization Constructs Using Higher-Order Separation Logic.
ACM Trans. Program. Lang. Syst.
Mike Dodds, Suresh Jagannathan, Matthew J. Parkinson, Kasper Svendsen, Lars Birkedal
2015 B conf
A Model of PCF in Guarded Type Theory.
MFPS
Marco Paviotti, Rasmus Ejlers Møgelberg, Lars Birkedal
2015 A conf
A Separation Logic for Fictional Sequential Consistency.
ESOP
Filip Sieczkowski, Kasper Svendsen, Lars Birkedal, Jean Pichon-Pharabod
2015 J jnl
Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191).
Dagstuhl Reports
Lars Birkedal, Derek Dreyer, Philippa Gardner, Zhong Shao
2015 A* conf
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning.
POPL
Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer
2015 B conf
ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages.
ITP
Filip Sieczkowski, Ales Bizjak, Lars Birkedal
2015 B conf
Programming and Reasoning with Guarded Recursion for Coinductive Types.
FoSSaCS
Ranald Clouston, Ales Bizjak, Hans Bugge Grathwohl, Lars Birkedal
2015 J jnl
Programming and Reasoning with Guarded Recursion for Coinductive Types.
CoRR
Ranald Clouston, Ales Bizjak, Hans Bugge Grathwohl, Lars Birkedal
2015 J jnl
Step-Indexed Logical Relations for Probability (long version).
CoRR
Ales Bizjak, Lars Birkedal
2015 B conf
Step-Indexed Logical Relations for Probability.
FoSSaCS
Ales Bizjak, Lars Birkedal
2014 — conf
A Model of Countable Nondeterminism in Guarded Type Theory.
RTA-TLCA
Ales Bizjak, Lars Birkedal, Marino Miculan
2014 A conf
Impredicative Concurrent Abstract Predicates.
ESOP
Kasper Svendsen, Lars Birkedal
2014 A* conf
Modular reasoning about concurrent higher-order imperative programs.
POPL
Lars Birkedal
2013 J jnl
A step-indexed Kripke model of hidden state.
Math. Struct. Comput. Sci.
Jan Schwinghammer, Lars Birkedal, François Pottier, Bernhard Reus, Kristian Støvring, Hongseok Yang
2013 J jnl
An inductive characterization of matching in binding bigraphs.
Formal Aspects Comput.
Troels Christoffer Damgaard, Arne J. Glenstrup, Lars Birkedal, Robin Milner
2013 A* conf
Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes.
LICS
Lars Birkedal, Rasmus Ejlers Møgelberg
2013 A conf
Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library.
ECOOP
Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson
2013 A* conf
Logical relations for fine-grained concurrency.
POPL
Aaron Joseph Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, Derek Dreyer
2013 A conf
Modular Reasoning about Separation of Concurrent Data Structures.
ESOP
Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson
2013 J jnl
Step-Indexed Relational Reasoning for Countable Nondeterminism.
Log. Methods Comput. Sci.
Lars Birkedal, Ales Bizjak, Jan Schwinghammer
2013 A conf
Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency.
ICFP
Aaron Turon, Derek Dreyer, Lars Birkedal
2013 A* conf
Views: compositional reasoning for concurrent programs.
POPL
Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, Hongseok Yang
2012 B conf
A Concurrent Logical Relation.
CSL
Lars Birkedal, Filip Sieczkowski, Jacob Thamsborg
2012 J jnl
A relational realizability model for higher-order stateful ADTs.
J. Log. Algebraic Methods Program.
Lars Birkedal, Kristian Støvring, Jacob Thamsborg
2012 B conf
Charge! - A Framework for Higher-Order Separation Logic in Coq.
ITP
Jesper Bengtson, Jonas Braband Jensen, Lars Birkedal
2012 A conf
Fictional Separation Logic.
ESOP
Jonas Braband Jensen, Lars Birkedal
2012 B conf
First Steps in Synthetic Guarded Domain Theory.
Advances in Modal Logic
Lars Birkedal
2012 J jnl
First steps in synthetic guarded domain theory: step-indexing in the topos of trees
Log. Methods Comput. Sci.
Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, Kristian Støvring
2012 — conf
Formalized Verification of Snapshotable Trees: Separation and Sharing.
VSTTE
Hannes Mehnert, Filip Sieczkowski, Lars Birkedal, Peter Sestoft
2012 B ed.
Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings
FoSSaCS
Lars Birkedal
2012 J jnl
The impact of higher-order state and control effects on local relational reasoning.
J. Funct. Program.
Derek Dreyer, Georg Neis, Lars Birkedal
2012 J jnl
Two for the Price of One: Lifting Separation Logic Assertions
Log. Methods Comput. Sci.
Jacob Thamsborg, Lars Birkedal, Hongseok Yang
2011 B conf
A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces.
FoSSaCS
Jan Schwinghammer, Lars Birkedal, Kristian Støvring
2011 A conf
A kripke logical relation for effect-based program transformations.
ICFP
Jacob Thamsborg, Lars Birkedal
2011 A* conf
First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees.
LICS
Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, Kristian Støvring
2011 J jnl
Logical Step-Indexed Logical Relations
Log. Methods Comput. Sci.
Derek Dreyer, Amal Ahmed, Lars Birkedal
2011 J jnl
Modular Verification of Linked Lists with Views via Separation Logic.
J. Object Technol.
Jonas Braband Jensen, Lars Birkedal, Peter Sestoft
2011 J jnl
Nested Hoare Triples and Frame Rules for Higher-order Store
Log. Methods Comput. Sci.
Jan Schwinghammer, Lars Birkedal, Bernhard Reus, Hongseok Yang
2011 — conf
Partiality, State and Dependent Types.
TLCA
Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski
2011 B conf
Step-Indexed Kripke Model of Separation Logic for Storable Locks.
MFPS
Alexandre Buisse, Lars Birkedal, Kristian Støvring
2011 B conf
Step-Indexed Relational Reasoning for Countable Nondeterminism.
CSL
Jan Schwinghammer, Lars Birkedal
2011 A* conf
Step-indexed kripke models over recursive worlds.
POPL
Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Kristian Støvring, Jacob Thamsborg, Hongseok Yang
2011 B conf
Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq.
ITP
Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski, Lars Birkedal
2010 — conf
10351 Abstracts Collection - Modelling, Controlling and Reasoning About State.
Modelling, Controlling and Reasoning About State
Amal Ahmed, Nick Benton, Lars Birkedal, Martin Hofmann
2010 — conf
10351 Executive Summary - Modelling, Controlling and Reasoning About State.
Modelling, Controlling and Reasoning About State
Amal Ahmed, Nick Benton, Lars Birkedal, Martin Hofmann
2010 — conf
A Metric Model of Lambda Calculus with Guarded Recursion.
FICS
Lars Birkedal, Jan Schwinghammer, Kristian Støvring
2010 B conf
A Semantic Foundation for Hidden State.
FoSSaCS
Jan Schwinghammer, Hongseok Yang, Lars Birkedal, François Pottier, Bernhard Reus
2010 — conf
A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces.
FICS
Lars Birkedal, Jan Schwinghammer, Kristian Støvring
2010 A* conf
A relational modal logic for higher-order stateful ADTs.
POPL
Derek Dreyer, Georg Neis, Andreas Rossberg, Lars Birkedal
2010 — ed.
Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010
Modelling, Controlling and Reasoning About State
Amal Ahmed, Nick Benton, Lars Birkedal, Martin Hofmann
2010 — conf
Modular verification of linked lists with views via separation logic.
FTfJP@ECOOP
Jonas Braband Jensen, Lars Birkedal, Peter Sestoft
2010 J jnl
Realisability semantics of parametric polymorphism, general references and recursive types.
Math. Struct. Comput. Sci.
Lars Birkedal, Kristian Støvring, Jacob Thamsborg
2010 J jnl
The category-theoretic solution of recursive metric-space equations.
Theor. Comput. Sci.
Lars Birkedal, Kristian Støvring, Jacob Thamsborg
2010 A conf
The impact of higher-order state and control effects on local relational reasoning.
ICFP
Derek Dreyer, Georg Neis, Lars Birkedal
2010 A conf
Verifying Generics and Delegates.
ECOOP
Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson
2010 — conf
Verifying event-driven programs using ramified frame properties.
TLDI
Neel Krishnaswami, Lars Birkedal, Jonathan Aldrich
2009 — conf
Design patterns in separation logic.
TLDI
Neelakantan R. Krishnaswami, Jonathan Aldrich, Lars Birkedal, Kasper Svendsen, Alexandre Buisse
2009 A* conf
Logical Step-Indexed Logical Relations.
LICS
Derek Dreyer, Amal Ahmed, Lars Birkedal
2009 B conf
Nested Hoare Triples and Frame Rules for Higher-Order Store.
CSL
Jan Schwinghammer, Lars Birkedal, Bernhard Reus, Hongseok Yang
2009 B conf
Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types.
FoSSaCS
Lars Birkedal, Kristian Støvring, Jacob Thamsborg
2009 — conf
Relational parametricity for references and recursive types.
TLDI
Lars Birkedal, Kristian Støvring, Jacob Thamsborg
2009 — conf
Solutions of Generalized Recursive Metric-Space Equations.
FICS
Lars Birkedal, Kristian Støvring, Jacob Thamsborg
2008 A conf
A Realizability Model for Impredicative Hoare Type Theory.
ESOP
Rasmus Lerchedahl Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett
2008 — conf
A Simple Model of Separation Logic for Higher-Order Store.
ICALP (2)
Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Hongseok Yang
2008 B conf
Higher-Order Separation Logic in Isabelle/HOLCF.
MFPS
Carsten Varming, Lars Birkedal
2008 J jnl
Hoare type theory, polymorphism and separation.
J. Funct. Program.
Aleksandar Nanevski, J. Gregory Morrisett, Lars Birkedal
2008 J jnl
Local reasoning about a copying garbage collector.
ACM Trans. Program. Lang. Syst.
Noah Torp-Smith, Lars Birkedal, John C. Reynolds
2008 B conf
On the Construction of Sorted Reactive Systems.
CONCUR
Lars Birkedal, Søren Debois, Thomas T. Hildebrandt
2008 J jnl
Relational Parametricity and Separation Logic
CoRR
Lars Birkedal, Hongseok Yang
2008 J jnl
Relational Parametricity and Separation Logic.
Log. Methods Comput. Sci.
Lars Birkedal, Hongseok Yang
2008 J jnl
Synthetic domain theory and models of linear Abadi & Plotkin logic.
Ann. Pure Appl. Log.
Rasmus Ejlers Møgelberg, Lars Birkedal, Giuseppe Rosolini
2008 A conf
Ynot: dependent types for imperative programs.
ICFP
Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, Lars Birkedal
2007 A conf
Abstract Predicates and Mutable ADTs in Hoare Type Theory.
ESOP
Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal
2007 J jnl
BI-hyperdoctrines, higher-order separation logic, and abstraction.
ACM Trans. Program. Lang. Syst.
Bodil Biering, Lars Birkedal, Noah Torp-Smith
2007 J jnl
Book Reviews.
Stud Logica
Lars Birkedal
2007 J jnl
Domain-theoretical models of parametric polymorphism.
Theor. Comput. Sci.
Lars Birkedal, Rasmus Ejlers Møgelberg, Rasmus Lerchedahl Petersen
2007 B conf
Relational Parametricity and Separation Logic.
FoSSaCS
Lars Birkedal, Hongseok Yang
2006 J jnl
Axiomatizing Binding Bigraphs.
Nord. J. Comput.
Troels Christoffer Damgaard, Lars Birkedal
2006 B conf
Bigraphical Models of Context-Aware Systems.
FoSSaCS
Lars Birkedal, Søren Debois, Ebbe Elsborg, Thomas T. Hildebrandt, Henning Niss
2006 J jnl
Linear Abadi and Plotkin Logic
CoRR
Lars Birkedal, Rasmus Ejlers Møgelberg, Rasmus Lerchedahl Petersen
2006 J jnl
Linear Abadi and Plotkin Logic.
Log. Methods Comput. Sci.
Lars Birkedal, Rasmus Ejlers Møgelberg, Rasmus Lerchedahl Petersen
2006 — conf
Matching of Bigraphs.
GT-VC@CONCUR
Lars Birkedal, Troels Christoffer Damgaard, Arne J. Glenstrup, Robin Milner
2006 A conf
Polymorphism and separation in hoare type theory.
ICFP
Aleksandar Nanevski, Greg Morrisett, Lars Birkedal
2006 B conf
Relational Reasoning for Recursive Types and References.
APLAS
Nina Bohr, Lars Birkedal
2006 J jnl
Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
CoRR
Lars Birkedal, Noah Torp-Smith, Hongseok Yang
2006 J jnl
Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages.
Log. Methods Comput. Sci.
Lars Birkedal, Noah Torp-Smith, Hongseok Yang
2006 B conf
Sortings for Reactive Systems.
CONCUR
Lars Birkedal, Søren Debois, Thomas T. Hildebrandt
2005 A conf
BI Hyperdoctrines and Higher-Order Separation Logic.
ESOP
Bodil Biering, Lars Birkedal, Noah Torp-Smith
2005 J jnl
Categorical models for Abadi and Plotkin's logic for parametricity.
Math. Struct. Comput. Sci.
Lars Birkedal, Rasmus Ejlers Møgelberg
2005 B conf
Parametric Domain-theoretic Models of Polymorphic Intuitionistic / Linear Lambda Calculus.
MFPS
Lars Birkedal, Rasmus Ejlers Møgelberg, Rasmus Lerchedahl Petersen
2005 — ed.
Proceedings of the 10th Conference on Category Theory in Computer Science, CTCS 2004, Copenhagen, Denmark, August 12-14, 2004
CTCS
Lars Birkedal
2005 A* conf
Semantics of Separation-Logic Typing and Higher-Order Frame Rules.
LICS
Lars Birkedal, Noah Torp-Smith, Hongseok Yang
2005 B conf
Synthetic Domain Theory and Models of Linear Abadi & Plotkin Logic.
MFPS
Rasmus Ejlers Møgelberg, Lars Birkedal, Giuseppe Rosolini
2004 J jnl
A Retrospective on Region-Based Memory Management.
High. Order Symb. Comput.
Mads Tofte, Lars Birkedal, Martin Elsman, Niels Hallenberg
2004 C conf
An infrastructure for context dependent mobile multimedia communication.
MMSP
J. Aa. Serensen, Kåre J. Kristoffersen, Andres Cervera, M. Schiortz, Thomas Lynge, Zoltan Safar, Lars Birkedal
2004 J jnl
Equilogical spaces.
Theor. Comput. Sci.
Andrej Bauer, Lars Birkedal, Dana S. Scott
2004 A* conf
Local reasoning about a copying garbage collector.
POPL
Lars Birkedal, Noah Torp-Smith, John C. Reynolds
2004 — conf
Preface.
CTCS
Lars Birkedal
2004 J jnl
Preface: Recent Developments in Domain Theory: A collection of papers in honour of Dana S. Scott.
Theor. Comput. Sci.
Lars Birkedal, Martín Hötzel Escardó, Achim Jung, Giuseppe Rosolini
2002 J jnl
A general notion of realizability.
Bull. Symb. Log.
Lars Birkedal
2002 J jnl
Local Realizability Toposes and a Modal Logic for Computability.
Math. Struct. Comput. Sci.
Steven Awodey, Lars Birkedal, Dana S. Scott
2002 J jnl
Relative and modified relative realizability.
Ann. Pure Appl. Log.
Lars Birkedal, Jaap van Oosten
2001 J jnl
A constraint-based region inference algorithm.
Theor. Comput. Sci.
Lars Birkedal, Mads Tofte
2000 A* conf
A General Notion of Realizability.
LICS
Lars Birkedal
2000 B conf
Continuous Functionals of Dependent Types and Equilogical Spaces.
CSL
Andrej Bauer, Lars Birkedal
2000 — book
Developing Theories of Types and Computability via Realizability.
Lars Birkedal
2000 — conf
Unification and polymorphism in region inference.
Proof, Language, and Interaction
Mads Tofte, Lars Birkedal
1999 — conf
Bibliography on Realizability.
Realizability Semantics and Applications@FLoC
Lars Birkedal
1999 — conf
Local Realizability Toposes and a Modal Logic for Computability.
Realizability Semantics and Applications@FLoC
Steven Awodey, Lars Birkedal, Dana S. Scott
1999 — conf
Preface.
Realizability Semantics and Applications@FLoC
Lars Birkedal, Jaap van Oosten, Giuseppe Rosolini, Dana S. Scott
1999 J jnl
Relational Interpretations of Recursive Types in an Operational Setting.
Inf. Comput.
Lars Birkedal, Robert Harper
1999 — ed.
Tutorial Workshop on Realizability Semantics and Applications, associated to FLoC'99, the 1999 Federated Logic Conference, Trento, Italy, June 30 - July 1, 1999
Realizability Semantics and Applications@FLoC
Lars Birkedal, Jaap van Oosten, Giuseppe Rosolini, Dana S. Scott
1998 J jnl
A Region Inference Algorithm.
ACM Trans. Program. Lang. Syst.
Mads Tofte, Lars Birkedal
1998 — conf
On propositions-as-types in realizability models.
Workshop on Domains
Lars Birkedal
1998 A* conf
Type Theory via Exact Categories.
LICS
Lars Birkedal, Aurelio Carboni, Giuseppe Rosolini, Dana S. Scott
1997 — conf
Relational Interpretations of Recursive Types in an operational Setting (Summary).
TACS
Lars Birkedal, Robert Harper
1996 A* conf
From Region Inference to von Neumann Machines via Region Representation Inference.
POPL
Lars Birkedal, Mads Tofte, Magnus Vejlstrup
1995 J jnl
Binding-Time Analysis for Standard ML.
LISP Symb. Comput.
Lars Birkedal, Morten Welinder
1994 C conf
Binding-Time Analysis for Standard ML.
PEPM
Lars Birkedal, Morten Welinder
1994 — conf
Hand-Writing Program Generator Generators.
PLILP
Lars Birkedal, Morten Welinder