Hand-Writing Program Generator Generators. - Lars Birkedal; Morten Welinder (PLILP, 1994)

Binding-Time Analysis for Standard ML. - Lars Birkedal; Morten Welinder (LISP Symb. Comput., 1995)

From Region Inference to von Neumann Machines via Region Representation Inference. - Lars Birkedal; Mads Tofte; Magnus Vejlstrup (POPL, 1996)

Relational Interpretations of Recursive Types in an operational Setting (Summary). - Lars Birkedal; Robert Harper 001 (TACS, 1997)

Type Theory via Exact Categories. - Lars Birkedal; Aurelio Carboni; Giuseppe Rosolini; Dana S. Scott (LICS, 1998)

On propositions-as-types in realizability models. - Lars Birkedal (Workshop on Domains, 1998)

A Region Inference Algorithm. - Mads Tofte; Lars Birkedal (ACM Trans. Program. Lang. Syst., 1998)

Local Realizability Toposes and a Modal Logic for Computability. - Steven Awodey; Lars Birkedal; Dana S. Scott (Realizability Semantics and Applications@FLoC, 1999)

Bibliography on Realizability. - Lars Birkedal (Realizability Semantics and Applications@FLoC, 1999)

Preface. - Lars Birkedal; Jaap van Oosten; Giuseppe Rosolini; Dana S. Scott (Realizability Semantics and Applications@FLoC, 1999)

Relational Interpretations of Recursive Types in an Operational Setting. - Lars Birkedal; Robert Harper 001 (Inf. Comput., 1999)

Unification and polymorphism in region inference. - Mads Tofte; Lars Birkedal (Proof, Language, and Interaction, 2000)

Continuous Functionals of Dependent Types and Equilogical Spaces. - Andrej Bauer; Lars Birkedal (CSL, 2000)

Developing Theories of Types and Computability via Realizability. - Lars Birkedal (Elsevier, 2000)

A constraint-based region inference algorithm. - Lars Birkedal; Mads Tofte (Theor. Comput. Sci., 2001)

Relative and modified relative realizability. - Lars Birkedal; Jaap van Oosten (Ann. Pure Appl. Log., 2002)

A general notion of realizability. - Lars Birkedal (Bull. Symb. Log., 2002)

An infrastructure for context dependent mobile multimedia communication. - J. Aa. Serensen; Kåre J. Kristoffersen; Andres Cervera; M. Schiortz; Thomas Lynge; Zoltan Safar; Lars Birkedal (MMSP, 2004)

A Retrospective on Region-Based Memory Management. - Mads Tofte; Lars Birkedal; Martin Elsman; Niels Hallenberg (High. Order Symb. Comput., 2004)

Equilogical spaces. - Andrej Bauer; Lars Birkedal; Dana S. Scott (Theor. Comput. Sci., 2004)

Preface: Recent Developments in Domain Theory: A collection of papers in honour of Dana S. Scott. - Lars Birkedal; Martín Hötzel Escardó; Achim Jung; Giuseppe Rosolini (Theor. Comput. Sci., 2004)

BI Hyperdoctrines and Higher-Order Separation Logic. - Bodil Biering; Lars Birkedal; Noah Torp-Smith (ESOP, 2005)

Semantics of Separation-Logic Typing and Higher-Order Frame Rules. - Lars Birkedal; Noah Torp-Smith; Hongseok Yang (LICS, 2005)

Parametric Domain-theoretic Models of Polymorphic Intuitionistic / Linear Lambda Calculus. - Lars Birkedal; Rasmus Ejlers Møgelberg; Rasmus Lerchedahl Petersen (MFPS, 2005)

Synthetic Domain Theory and Models of Linear Abadi & Plotkin Logic. - Rasmus Ejlers Møgelberg; Lars Birkedal; Giuseppe Rosolini (MFPS, 2005)

Categorical models for Abadi and Plotkin's logic for parametricity. - Lars Birkedal; Rasmus Ejlers Møgelberg (Math. Struct. Comput. Sci., 2005)

Relational Reasoning for Recursive Types and References. - Nina Bohr; Lars Birkedal (APLAS, 2006)

Sortings for Reactive Systems. - Lars Birkedal; Søren Debois; Thomas T. Hildebrandt (CONCUR, 2006)

Bigraphical Models of Context-Aware Systems. - Lars Birkedal; Søren Debois; Ebbe Elsborg; Thomas T. Hildebrandt; Henning Niss (FoSSaCS, 2006)

Polymorphism and separation in hoare type theory. - Aleksandar Nanevski; Greg Morrisett; Lars Birkedal (ICFP, 2006)

Matching of Bigraphs. - Lars Birkedal; Troels Christoffer Damgaard; Arne J. Glenstrup; Robin Milner (GT-VC@CONCUR, 2006)

Linear Abadi and Plotkin Logic. - Lars Birkedal; Rasmus Ejlers Møgelberg; Rasmus Lerchedahl Petersen (Log. Methods Comput. Sci., 2006)

Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages. - Lars Birkedal; Noah Torp-Smith; Hongseok Yang (Log. Methods Comput. Sci., 2006)

Axiomatizing Binding Bigraphs. - Troels Christoffer Damgaard; Lars Birkedal (Nord. J. Comput., 2006)

Abstract Predicates and Mutable ADTs in Hoare Type Theory. - Aleksandar Nanevski; Amal Ahmed 001; Greg Morrisett; Lars Birkedal (ESOP, 2007)

Book Reviews. - Lars Birkedal (Stud Logica, 2007)

Domain-theoretical models of parametric polymorphism. - Lars Birkedal; Rasmus Ejlers Møgelberg; Rasmus Lerchedahl Petersen (Theor. Comput. Sci., 2007)

BI-hyperdoctrines, higher-order separation logic, and abstraction. - Bodil Biering; Lars Birkedal; Noah Torp-Smith (ACM Trans. Program. Lang. Syst., 2007)

On the Construction of Sorted Reactive Systems. - Lars Birkedal; Søren Debois; Thomas T. Hildebrandt (CONCUR, 2008)

A Realizability Model for Impredicative Hoare Type Theory. - Rasmus Lerchedahl Petersen; Lars Birkedal; Aleksandar Nanevski; Greg Morrisett (ESOP, 2008)

A Simple Model of Separation Logic for Higher-Order Store. - Lars Birkedal; Bernhard Reus; Jan Schwinghammer; Hongseok Yang (ICALP (2), 2008)

Ynot: dependent types for imperative programs. - Aleksandar Nanevski; Greg Morrisett; Avraham Shinnar; Paul Govereau; Lars Birkedal (ICFP, 2008)

Higher-Order Separation Logic in Isabelle/HOLCF. - Carsten Varming; Lars Birkedal (MFPS, 2008)

Hoare type theory, polymorphism and separation. - Aleksandar Nanevski; J. Gregory Morrisett; Lars Birkedal (J. Funct. Program., 2008)

Relational Parametricity and Separation Logic. - Lars Birkedal; Hongseok Yang (Log. Methods Comput. Sci., 2008)

Local reasoning about a copying garbage collector. - Noah Torp-Smith; Lars Birkedal; John C. Reynolds (ACM Trans. Program. Lang. Syst., 2008)

Solutions of Generalized Recursive Metric-Space Equations. - Lars Birkedal; Kristian Støvring; Jacob Thamsborg (FICS, 2009)

Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types. - Lars Birkedal; Kristian Støvring; Jacob Thamsborg (FoSSaCS, 2009)

Relational parametricity for references and recursive types. - Lars Birkedal; Kristian Støvring; Jacob Thamsborg (TLDI, 2009)

Design patterns in separation logic. - Neelakantan R. Krishnaswami; Jonathan Aldrich; Lars Birkedal; Kasper Svendsen; Alexandre Buisse (TLDI, 2009)

10351 Abstracts Collection - Modelling, Controlling and Reasoning About State. - Amal Ahmed 001; Nick Benton; Lars Birkedal; Martin Hofmann 001 (Modelling, Controlling and Reasoning About State, 2010)

10351 Executive Summary - Modelling, Controlling and Reasoning About State. - Amal Ahmed 001; Nick Benton; Lars Birkedal; Martin Hofmann 001 (Modelling, Controlling and Reasoning About State, 2010)

Verifying Generics and Delegates. - Kasper Svendsen; Lars Birkedal; Matthew J. Parkinson (ECOOP, 2010)

A Metric Model of Lambda Calculus with Guarded Recursion. - Lars Birkedal; Jan Schwinghammer; Kristian Støvring (FICS, 2010)

A Semantic Foundation for Hidden State. - Jan Schwinghammer; Hongseok Yang; Lars Birkedal; François Pottier; Bernhard Reus (FoSSaCS, 2010)

A relational modal logic for higher-order stateful ADTs. - Derek Dreyer; Georg Neis; Andreas Rossberg; Lars Birkedal (POPL, 2010)

Verifying event-driven programs using ramified frame properties. - Neel Krishnaswami; Lars Birkedal; Jonathan Aldrich (TLDI, 2010)

Realisability semantics of parametric polymorphism, general references and recursive types. - Lars Birkedal; Kristian Støvring; Jacob Thamsborg (Math. Struct. Comput. Sci., 2010)

The category-theoretic solution of recursive metric-space equations. - Lars Birkedal; Kristian Støvring; Jacob Thamsborg (Theor. Comput. Sci., 2010)

Step-Indexed Relational Reasoning for Countable Nondeterminism. - Jan Schwinghammer; Lars Birkedal (CSL, 2011)

A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces. - Jan Schwinghammer; Lars Birkedal; Kristian Støvring (FoSSaCS, 2011)

A kripke logical relation for effect-based program transformations. - Jacob Thamsborg; Lars Birkedal (ICFP, 2011)

Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq. - Jesper Bengtson; Jonas Braband Jensen; Filip Sieczkowski; Lars Birkedal (ITP, 2011)

Step-indexed kripke models over recursive worlds. - Lars Birkedal; Bernhard Reus; Jan Schwinghammer; Kristian Støvring; Jacob Thamsborg; Hongseok Yang (POPL, 2011)

Partiality, State and Dependent Types. - Kasper Svendsen; Lars Birkedal; Aleksandar Nanevski (TLCA, 2011)

Logical Step-Indexed Logical Relations - Derek Dreyer; Amal Ahmed 001; Lars Birkedal (Log. Methods Comput. Sci., 2011)

Nested Hoare Triples and Frame Rules for Higher-order Store - Jan Schwinghammer; Lars Birkedal; Bernhard Reus; Hongseok Yang (Log. Methods Comput. Sci., 2011)

Step-Indexed Kripke Model of Separation Logic for Storable Locks. - Alexandre Buisse; Lars Birkedal; Kristian Støvring (MFPS, 2011)

Modular Verification of Linked Lists with Views via Separation Logic. - Jonas Braband Jensen; Lars Birkedal; Peter Sestoft (J. Object Technol., 2011)

First Steps in Synthetic Guarded Domain Theory. - Lars Birkedal (Advances in Modal Logic, 2012)

A Concurrent Logical Relation. - Lars Birkedal; Filip Sieczkowski; Jacob Thamsborg (CSL, 2012)

Fictional Separation Logic. - Jonas Braband Jensen; Lars Birkedal (ESOP, 2012)

Charge! - A Framework for Higher-Order Separation Logic in Coq. - Jesper Bengtson; Jonas Braband Jensen; Lars Birkedal (ITP, 2012)

Formalized Verification of Snapshotable Trees: Separation and Sharing. - Hannes Mehnert; Filip Sieczkowski; Lars Birkedal; Peter Sestoft (VSTTE, 2012)

First steps in synthetic guarded domain theory: step-indexing in the topos of trees - Lars Birkedal; Rasmus Ejlers Møgelberg; Jan Schwinghammer; Kristian Støvring (Log. Methods Comput. Sci., 2012)

Two for the Price of One: Lifting Separation Logic Assertions - Jacob Thamsborg; Lars Birkedal; Hongseok Yang (Log. Methods Comput. Sci., 2012)

The impact of higher-order state and control effects on local relational reasoning. - Derek Dreyer; Georg Neis; Lars Birkedal (J. Funct. Program., 2012)

A relational realizability model for higher-order stateful ADTs. - Lars Birkedal; Kristian Støvring; Jacob Thamsborg (J. Log. Algebraic Methods Program., 2012)

Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library. - Kasper Svendsen; Lars Birkedal; Matthew J. Parkinson (ECOOP, 2013)

Modular Reasoning about Separation of Concurrent Data Structures. - Kasper Svendsen; Lars Birkedal; Matthew J. Parkinson (ESOP, 2013)

Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. - Aaron Turon; Derek Dreyer; Lars Birkedal (ICFP, 2013)

Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes. - Lars Birkedal; Rasmus Ejlers Møgelberg (LICS, 2013)

Views: compositional reasoning for concurrent programs. - Thomas Dinsdale-Young; Lars Birkedal; Philippa Gardner; Matthew J. Parkinson; Hongseok Yang (POPL, 2013)

Logical relations for fine-grained concurrency. - Aaron Joseph Turon; Jacob Thamsborg; Amal Ahmed 001; Lars Birkedal; Derek Dreyer (POPL, 2013)

Step-Indexed Relational Reasoning for Countable Nondeterminism. - Lars Birkedal; Ales Bizjak; Jan Schwinghammer (Log. Methods Comput. Sci., 2013)

An inductive characterization of matching in binding bigraphs. - Troels Christoffer Damgaard; Arne J. Glenstrup; Lars Birkedal; Robin Milner (Formal Aspects Comput., 2013)

A step-indexed Kripke model of hidden state. - Jan Schwinghammer; Lars Birkedal; François Pottier; Bernhard Reus; Kristian Støvring; Hongseok Yang (Math. Struct. Comput. Sci., 2013)

Impredicative Concurrent Abstract Predicates. - Kasper Svendsen; Lars Birkedal (ESOP, 2014)

Modular reasoning about concurrent higher-order imperative programs. - Lars Birkedal (POPL, 2014)

A Model of Countable Nondeterminism in Guarded Type Theory. - Ales Bizjak; Lars Birkedal; Marino Miculan (RTA-TLCA, 2014)

A Separation Logic for Fictional Sequential Consistency. - Filip Sieczkowski; Kasper Svendsen; Lars Birkedal; Jean Pichon-Pharabod (ESOP, 2015)

Step-Indexed Logical Relations for Probability. - Ales Bizjak; Lars Birkedal (FoSSaCS, 2015)

Programming and Reasoning with Guarded Recursion for Coinductive Types. - Ranald Clouston; Ales Bizjak; Hans Bugge Grathwohl; Lars Birkedal (FoSSaCS, 2015)

ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages. - Filip Sieczkowski; Ales Bizjak; Lars Birkedal (ITP, 2015)

Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. - Ralf Jung 002; David Swasey; Filip Sieczkowski; Kasper Svendsen; Aaron Turon; Lars Birkedal; Derek Dreyer (POPL, 2015)

Step-Indexed Logical Relations for Probability (long version). - Ales Bizjak; Lars Birkedal (CoRR, 2015)

Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191). - Lars Birkedal; Derek Dreyer; Philippa Gardner; Zhong Shao 001 (Dagstuhl Reports, 2015)

A Model of PCF in Guarded Type Theory. - Marco Paviotti; Rasmus Ejlers Møgelberg; Lars Birkedal (MFPS, 2015)

Guarded Cubical Type Theory: Path Equality for Guarded Recursion. - Lars Birkedal; Ales Bizjak; Ranald Clouston; Hans Bugge Grathwohl; Bas Spitters; Andrea Vezzosi (CSL, 2016)

Transfinite Step-Indexing: Decoupling Concrete and Logical Steps. - Kasper Svendsen; Filip Sieczkowski; Lars Birkedal (ESOP, 2016)

Reasoning about Object Capabilities with Logical Relations and Effect Parametricity. - Dominique Devriese; Lars Birkedal; Frank Piessens (EuroS&P, 2016)

Guarded Dependent Type Theory with Coinductive Types. - Ales Bizjak; Hans Bugge Grathwohl; Ranald Clouston; Rasmus Ejlers Møgelberg; Lars Birkedal (FoSSaCS, 2016)

Higher-order ghost state. - Ralf Jung 002; Robbert Krebbers; Lars Birkedal; Derek Dreyer (ICFP, 2016)

The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. - Ranald Clouston; Ales Bizjak; Hans Bugge Grathwohl; Lars Birkedal (Log. Methods Comput. Sci., 2016)

Preface. - Lars Birkedal (MFPS, 2016)

A Kripke logical relation for effect-based program transformations. - Lars Birkedal; Guilhem Jaber; Filip Sieczkowski; Jacob Thamsborg (Inf. Comput., 2016)

Verifying Custom Synchronization Constructs Using Higher-Order Separation Logic. - Mike Dodds; Suresh Jagannathan; Matthew J. Parkinson; Kasper Svendsen; Lars Birkedal (ACM Trans. Program. Lang. Syst., 2016)

Caper - Automatic Verification for Fine-Grained Concurrency. - Thomas Dinsdale-Young; Pedro da Rocha Pinto; Kristoffer Just Andersen; Lars Birkedal (ESOP, 2017)

The Essence of Higher-Order Concurrent Separation Logic. - Robbert Krebbers; Ralf Jung 002; Ales Bizjak; Jacques-Henri Jourdan; Derek Dreyer; Lars Birkedal (ESOP, 2017)

Interactive proofs in higher-order concurrent separation logic. - Robbert Krebbers; Amin Timany; Lars Birkedal (POPL, 2017)

A relational model of types-and-effects in higher-order concurrent separation logic. - Morten Krogh-Jespersen; Kasper Svendsen; Lars Birkedal (POPL, 2017)

Trace Properties from Separation Logic Specifications. - Lars Birkedal; Thomas Dinsdale-Young; Guilhem Jaber; Kasper Svendsen; Nikos Tzevelekos (CoRR, 2017)

Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. - Alejandro Aguirre 001; Gilles Barthe; Lars Birkedal; Ales Bizjak; Marco Gaboardi; Deepak Garg 001 (ESOP, 2018)

ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. - Dan Frumin; Robbert Krebbers; Lars Birkedal (LICS, 2018)

Compositional Non-interference for Concurrent Programs via Separation and Framing. - Aleksandr Karbyshev; Kasper Svendsen; Aslan Askarov; Lars Birkedal (POST, 2018)

StkTokens: Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities - Technical Report with Proofs and Details. - Lau Skorstengaard; Dominique Devriese; Lars Birkedal (CoRR, 2018)

On Models of Higher-Order Separation Logic. - Ales Bizjak; Lars Birkedal (MFPS, 2018)

Iris from the ground up: A modular foundation for higher-order concurrent separation logic. - Ralf Jung 002; Robbert Krebbers; Jacques-Henri Jourdan; Ales Bizjak; Lars Birkedal; Derek Dreyer (J. Funct. Program., 2018)

A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST. - Amin Timany; Léo Stefanesco; Morten Krogh-Jespersen; Lars Birkedal (Proc. ACM Program. Lang., 2018)

A model of guarded recursion via generalised equilogical spaces. - Ales Bizjak; Lars Birkedal (Theor. Comput. Sci., 2018)

Reasoning About a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management - Technical Appendix Including Proofs and Details. - Lau Skorstengaard; Dominique Devriese; Lars Birkedal (CoRR, 2019)

Guarded Cubical Type Theory. - Lars Birkedal; Ales Bizjak; Ranald Clouston; Hans Bugge Grathwohl; Bas Spitters; Andrea Vezzosi (J. Autom. Reason., 2019)

Iron: managing obligations in higher-order concurrent separation logic. - Ales Bizjak; Daniel Gratzer; Robbert Krebbers; Lars Birkedal (Proc. ACM Program. Lang., 2019)

Implementing a modal dependent type theory. - Daniel Gratzer; Jonathan Sterling; Lars Birkedal (Proc. ACM Program. Lang., 2019)

StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities. - Lau Skorstengaard; Dominique Devriese; Lars Birkedal (Proc. ACM Program. Lang., 2019)

Mechanized relational verification of concurrent programs with continuations. - Amin Timany; Lars Birkedal (Proc. ACM Program. Lang., 2019)

Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. - Morten Krogh-Jespersen; Amin Timany; Marit Edna Ohlenbusch; Simon Oddershede Gregersen; Lars Birkedal (ESOP, 2020)

Modal dependent type theory and dependent right adjoints. - Lars Birkedal; Ranald Clouston; Bassel Mannaa; Rasmus Ejlers Møgelberg; Andrew M. Pitts; Bas Spitters (Math. Struct. Comput. Sci., 2020)

Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris. - Paolo G. Giarrusso; Léo Stefanesco; Amin Timany; Lars Birkedal; Robbert Krebbers (Proc. ACM Program. Lang., 2020)

Reasoning about a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management. - Lau Skorstengaard; Dominique Devriese; Lars Birkedal (ACM Trans. Program. Lang. Syst., 2020)

Contextual Refinement of the Michael-Scott Queue - Coq Artifact. - Simon Friis Vindum; Lars Birkedal (Zenodo, 2020)

Reasoning about monotonicity in separation logic. - Amin Timany; Lars Birkedal (CPP, 2021)

Contextual refinement of the Michael-Scott queue (proof pearl). - Simon Friis Vindum; Lars Birkedal (CPP, 2021)

Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. - Simon Spies; Lennard Gäher; Daniel Gratzer; Joseph Tassarotti; Robbert Krebbers; Derek Dreyer; Lars Birkedal (PLDI, 2021)

Compositional Non-Interference for Fine-Grained Concurrent Programs. - Dan Frumin; Robbert Krebbers; Lars Birkedal (SP, 2021)

Trillium: Unifying Refinement and Higher-Order Distributed Separation Logic. - Amin Timany; Simon Oddershede Gregersen; Léo Stefanesco; Léon Gondelman; Abel Nieto; Lars Birkedal (CoRR, 2021)

ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. - Dan Frumin; Robbert Krebbers; Lars Birkedal (Log. Methods Comput. Sci., 2021)

Multimodal Dependent Type Theory. - Daniel Gratzer; G. A. Kavvos; Andreas Nuyts; Lars Birkedal (Log. Methods Comput. Sci., 2021)

Theorems for free from separation logic specifications. - Lars Birkedal; Thomas Dinsdale-Young; Armaël Guéneau; Guilhem Jaber; Kasper Svendsen; Nikos Tzevelekos (Proc. ACM Program. Lang., 2021)

Efficient and provable local capability revocation using uninitialized capabilities. - Aïna Linn Georges; Armaël Guéneau; Thomas Van Strydonck; Amin Timany; Alix Trieu; Sander Huyghebaert; Dominique Devriese; Lars Birkedal (Proc. ACM Program. Lang., 2021)

Distributed causal memory: modular specification and verification in higher-order distributed separation logic. - Léon Gondelman; Simon Oddershede Gregersen; Abel Nieto; Amin Timany; Lars Birkedal (Proc. ACM Program. Lang., 2021)

Mechanized logical relations for termination-insensitive noninterference. - Simon Oddershede Gregersen; Johan Bay; Amin Timany; Lars Birkedal (Proc. ACM Program. Lang., 2021)

Client-server sessions in linear logic. - Zesen Qian; G. A. Kavvos; Lars Birkedal (Proc. ACM Program. Lang., 2021)

Proving full-system security properties under multiple attacker models on capability machines: Coq mechanization. - Thomas Van Strydonck; Aïna Linn Georges; Armaël Guéneau; Alix Trieu; Amin Timany; Frank Piessens; Lars Birkedal; Dominique Devriese (Zenodo, 2021)

Mechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Library - Coq Artefact. - Simon Friis Vindum; Dan Frumin; Lars Birkedal (Zenodo, 2021)

Coq development for "Mechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Library". - Simon Friis Vindum; Dan Frumin; Lars Birkedal (Zenodo, 2021)

Mechanized verification of a fine-grained concurrent queue from meta's folly library. - Simon Friis Vindum; Dan Frumin; Lars Birkedal (CPP, 2022)

Proving full-system security properties under multiple attacker models on capability machines. - Thomas Van Strydonck; Aïna Linn Georges; Armaël Guéneau; Alix Trieu; Amin Timany; Frank Piessens; Lars Birkedal; Dominique Devriese (CSF, 2022)

A Stratified Approach to Löb Induction. - Daniel Gratzer; Lars Birkedal (FSCD, 2022)

{mitten}: A Flexible Multimodal Proof Assistant. - Philipp Stassen; Daniel Gratzer; Lars Birkedal (TYPES, 2022)

Denotational semantics of general store and polymorphism. - Jonathan Sterling; Daniel Gratzer; Lars Birkedal (CoRR, 2022)

Controlling unfolding in type theory. - Daniel Gratzer; Jonathan Sterling; Carlo Angiuli; Thierry Coquand; Lars Birkedal (CoRR, 2022)

Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities. - Aïna Linn Georges; Alix Trieu; Lars Birkedal (Proc. ACM Program. Lang., 2022)

Modular verification of op-based CRDTs in separation logic. - Abel Nieto; Léon Gondelman; Alban Reynaud; Amin Timany; Lars Birkedal (Proc. ACM Program. Lang., 2022)

Later credits: resourceful reasoning for the later modality. - Simon Spies; Lennard Gäher; Joseph Tassarotti; Ralf Jung 002; Robbert Krebbers; Lars Birkedal; Derek Dreyer (Proc. ACM Program. Lang., 2022)

Modalities and Parametric Adjoints. - Daniel Gratzer; Evan Cavallo; G. A. Kavvos; Adrien Guatto; Lars Birkedal (ACM Trans. Comput. Log., 2022)

Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities (Artifact). - Aïna Linn Georges; Alix Trieu; Lars Birkedal (Zenodo, 2022)

Modular Verification of Op-Based CRDTs in Separation Logic (Proof Artifact). - Abel Nieto; Léon Gondelman; Alban Reynaud; Amin Timany; Lars Birkedal (Zenodo, 2022)

Modular Verification of Op-Based CRDTs in Separation Logic (Proof Artifact). - Abel Nieto; Léon Gondelman; Alban Reynaud; Amin Timany; Lars Birkedal (Zenodo, 2022)

Modular Verification of State-Based CRDTs in Separation Logic. - Abel Nieto; Arnaud Daby-Seesaram; Léon Gondelman; Amin Timany; Lars Birkedal (ECOOP, 2023)

Free theorems from univalent reference types. - Jonathan Sterling; Daniel Gratzer; Lars Birkedal (CoRR, 2023)

A denotationally-based program logic for higher-order store. - Frederik Lerbjerg Aagaard; Jonathan Sterling; Lars Birkedal (MFPS, 2023)

Modular Verification of State-Based CRDTs in Separation Logic (Artifact). - Abel Nieto; Arnaud Daby-Seesaram; Léon Gondelman; Amin Timany; Lars Birkedal (Dagstuhl Artifacts Ser., 2023)

VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A. - Zongyuan Liu 001; Sergei Stepanenko; Jean Pichon-Pharabod; Amin Timany; Aslan Askarov; Lars Birkedal (Proc. ACM Program. Lang., 2023)

Iris-Wasm: Robust and Modular Verification of WebAssembly Programs. - Xiaojia Rao; Aïna Linn Georges; Maxime Legoupil; Conrad Watt; Jean Pichon-Pharabod; Philippa Gardner; Lars Birkedal (Proc. ACM Program. Lang., 2023)

Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice. - Alejandro Aguirre 001; Lars Birkedal (Proc. ACM Program. Lang., 2023)

Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols. - Léon Gondelman; Jonas Kastberg Hinrichsen; Mário Pereira; Amin Timany; Lars Birkedal (Proc. ACM Program. Lang., 2023)

Artifact for the paper "Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory" in OOPSLA23. - Simon Friis Vindum; Lars Birkedal (Zenodo, 2023)

Artifact for the paper "Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory" in OOPSLA23. - Simon Friis Vindum; Lars Birkedal (Zenodo, 2023)

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic - Coq Artifact. - Simon Oddershede Gregersen; Alejandro Aguirre 001; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal (Zenodo, 2023)

The Essence of Generalized Algebraic Data Types. - Filip Sieczkowski; Sergei Stepanenko; Jonathan Sterling; Lars Birkedal (Zenodo, 2023)

The Essence of Generalized Algebraic Data Types. - Filip Sieczkowski; Sergei Stepanenko; Jonathan Sterling; Lars Birkedal (Zenodo, 2023)

The Essence of Generalized Algebraic Data Types. - Filip Sieczkowski; Sergei Stepanenko; Jonathan Sterling; Lars Birkedal (Zenodo, 2023)

Melocoton: A Program Logic for Verified Interoperability Between OCaml and C. - Armaël Guéneau; Johannes Hostert; Simon Spies; Michael Sammler; Lars Birkedal; Derek Dreyer (Proc. ACM Program. Lang., 2023)

Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory. - Simon Friis Vindum; Lars Birkedal (Proc. ACM Program. Lang., 2023)

The Logical Essence of Well-Bracketed Control Flow (Artifact). - Amin Timany; Armaël Guéneau; Lars Birkedal (Zenodo, 2023)

The Logical Essence of Well-Bracketed Control Flow (Artifact). - Amin Timany; Armaël Guéneau; Lars Birkedal (Zenodo, 2023)

The Logical Essence of Well-Bracketed Control Flow (Artifact). - Amin Timany; Armaël Guéneau; Lars Birkedal (Zenodo, 2023)

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement - Coq Artifact. - Amin Timany; Simon Oddershede Gregersen; Léo Stefanesco; Jonas Kastberg Hinrichsen; Léon Gondelman; Abel Nieto; Lars Birkedal (Zenodo, 2023)

Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics. - Jonathan Sterling; Daniel Gratzer; Lars Birkedal (CSL, 2024)

Modelling Probabilistic FPC in Guarded Type Theory. - Philipp Stassen; Rasmus Ejlers Møgelberg; Maaike Zwart; Alejandro Aguirre 001; Lars Birkedal (CoRR, 2024)

Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code. - Aïna Linn Georges; Armaël Guéneau; Thomas Van Strydonck; Amin Timany; Alix Trieu; Dominique Devriese; Lars Birkedal (J. ACM, 2024)

Unifying cubical and multimodal type theory. - Frederik Lerbjerg Aagaard; Magnus Baunsgaard Kristensen; Daniel Gratzer; Lars Birkedal (Log. Methods Comput. Sci., 2024)

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs. - Alejandro Aguirre 001; Philipp G. Haselwarter; Markus de Medeiros; Kwing Hei Li; Simon Oddershede Gregersen; Joseph Tassarotti; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Almost-Sure Termination by Guarded Refinement. - Simon Oddershede Gregersen; Alejandro Aguirre 001; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Tachis: Higher-Order Separation Logic with Credits for Expected Costs. - Philipp G. Haselwarter; Kwing Hei Li; Markus de Medeiros; Simon Oddershede Gregersen; Alejandro Aguirre 001; Joseph Tassarotti; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly. - Maxime Legoupil; June Rousseau; Aïna Linn Georges; Jean Pichon-Pharabod; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Modular Denotational Semantics for Effects with Guarded Interaction Trees. - Dan Frumin; Amin Timany; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. - Simon Oddershede Gregersen; Alejandro Aguirre 001; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal (Proc. ACM Program. Lang., 2024)

An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic. - Angus Hammond; Zongyuan Liu 001; Thibaut Pérami; Peter Sewell; Lars Birkedal; Jean Pichon-Pharabod (Proc. ACM Program. Lang., 2024)

The Essence of Generalized Algebraic Data Types. - Filip Sieczkowski; Sergei Stepanenko; Jonathan Sterling; Lars Birkedal (Proc. ACM Program. Lang., 2024)

The Logical Essence of Well-Bracketed Control Flow. - Amin Timany; Armaël Guéneau; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement. - Amin Timany; Simon Oddershede Gregersen; Léo Stefanesco; Jonas Kastberg Hinrichsen; Léon Gondelman; Abel Nieto; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs - Coq Artifact. - Alejandro Aguirre 001; Philipp G. Haselwarter; Markus de Medeiros; Kwing Hei Li; Simon Oddershede Gregersen; Joseph Tassarotti; Lars Birkedal (Zenodo, 2024)

Almost-Sure Termination by Guarded Refinement - Coq Artifact. - Simon Oddershede Gregersen; Alejandro Aguirre 001; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal (Zenodo, 2024)

Artifact and Appendix of 'Iris-MSWasm: elucidating and mechanising the security invariants of Memory-Safe WebAssembly'. - Maxime Legoupil; June Rousseau; Aïna Linn Georges; Jean Pichon-Pharabod; Lars Birkedal (Zenodo, 2024)

Approximate Relational Reasoning for Higher-Order Probabilistic Programs - Formalization Artifact. - Philipp G. Haselwarter; Kwing Hei Li; Alejandro Aguirre 001; Simon Oddershede Gregersen; Joseph Tassarotti; Lars Birkedal (Zenodo, 2024)

A Logical Approach to Type Soundness. - Amin Timany; Robbert Krebbers; Derek Dreyer; Lars Birkedal (J. ACM, 2024)

The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic. - Simon Friis Vindum; Aïna Linn Georges; Lars Birkedal (CPP, 2025)

Context-Dependent Effects in Guarded Interaction Trees. - Sergei Stepanenko; Emma Nardino; Dan Frumin; Amin Timany; Lars Birkedal (ESOP (2), 2025)

Idempotent Resources in Separation Logic - The Heart of core in Iris. - Daniel Gratzer; Mathias Adam Møller; Lars Birkedal (FoSSaCS, 2025)

Approximate Relational Reasoning for Higher-Order Probabilistic Programs. - Philipp G. Haselwarter; Kwing Hei Li; Alejandro Aguirre 001; Simon Oddershede Gregersen; Joseph Tassarotti; Lars Birkedal (Proc. ACM Program. Lang., 2025)

Modelling Recursion and Probabilistic Choice in Guarded Type Theory. - Philipp Stassen; Rasmus Ejlers Møgelberg; Maaike Zwart; Alejandro Aguirre 001; Lars Birkedal (Proc. ACM Program. Lang., 2025)

Context-Dependent Effects in Guarded Interaction Trees. - Sergei Stepanenko; Emma Nardino; Dan Frumin; Amin Timany; Lars Birkedal (Zenodo, 2025)

Reasoning about Weak Isolation Levels in Separation Logic. - Anders Alnor Mathiasen; Léon Gondelman; Léon Ducruet; Amin Timany; Lars Birkedal (CoRR, 2025)

Context-Dependent Effects in Guarded Interaction Trees. - Sergei Stepanenko; Emma Nardino; Dan Frumin; Amin Timany; Lars Birkedal (Zenodo, 2025)

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs. - Kwing Hei Li; Alejandro Aguirre 001; Simon Oddershede Gregersen; Philipp G. Haselwarter; Joseph Tassarotti; Lars Birkedal (CoRR, 2025)