| 2026 | CPP | Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic. | Virgil Marionneau, Flix Sassus Bourda, Alejandro Aguirre, Lars Birkedal |
| 2026 | ECOOP | Verifying Wait-Freedom for Concurrent Higher-Order Programs. | Egor Namakonov, Lars Birkedal, Amin Timany |
| 2026 | LICS | Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic. | Markus de Medeiros, Puming Liu, Kwing Hei Li, Alejandro Aguirre, Lars Birkedal, Joseph Tassarotti |
| 2025 | CPP | The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic. | Simon Friis Vindum, Ana Linn Georges, Lars Birkedal |
| 2025 | ESOP | Context-Dependent Effects in Guarded Interaction Trees. | Sergei Stepanenko, Emma Nardino, Dan Frumin, Amin Timany, Lars Birkedal |
| 2025 | FOSSACS | Idempotent Resources in Separation Logic - The Heart of core in Iris. | Daniel Gratzer, Mathias Adam Mller, Lars Birkedal |
| 2024 | CSL | Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics. | Jonathan Sterling, Daniel Gratzer, Lars Birkedal |
| 2023 | ECOOP | Modular Verification of State-Based CRDTs in Separation Logic. | Abel Nieto, Arnaud Daby-Seesaram, Lon Gondelman, Amin Timany, Lars Birkedal |
| 2022 | CPP | Mechanized verification of a fine-grained concurrent queue from meta's folly library. | Simon Friis Vindum, Dan Frumin, Lars Birkedal |
| 2022 | FSCD | A Stratified Approach to Lb Induction. | Daniel Gratzer, Lars Birkedal |
| 2021 | CPP | Reasoning about monotonicity in separation logic. | Amin Timany, Lars Birkedal |
| 2021 | CPP | Contextual refinement of the Michael-Scott queue (proof pearl). | Simon Friis Vindum, Lars Birkedal |
| 2021 | PLDI | Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. | Simon Spies, Lennard Gher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal |
| 2021 | SP | Compositional Non-Interference for Fine-Grained Concurrent Programs. | Dan Frumin, Robbert Krebbers, Lars Birkedal |
| 2020 | ESOP | Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. | Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, Lars Birkedal |
| 2020 | LICS | Multimodal Dependent Type Theory. | Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal |
| 2018 | ESOP | Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. | Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg |
| 2018 | ESOP | Reasoning About a Machine with Local Capabilities - Provably Safe Stack and Return Pointer Management. | Lau Skorstengaard, Dominique Devriese, Lars Birkedal |
| 2018 | LICS | ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. | Dan Frumin, Robbert Krebbers, Lars Birkedal |
| 2017 | ESOP | Caper - Automatic Verification for Fine-Grained Concurrency. | Thomas Dinsdale-Young, Pedro da Rocha Pinto, Kristoffer Just Andersen, Lars Birkedal |
| 2017 | ESOP | The Essence of Higher-Order Concurrent Separation Logic. | Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal |
| 2017 | POPL | Interactive proofs in higher-order concurrent separation logic. | Robbert Krebbers, Amin Timany, Lars Birkedal |
| 2017 | POPL | A relational model of types-and-effects in higher-order concurrent separation logic. | Morten Krogh-Jespersen, Kasper Svendsen, Lars Birkedal |
| 2016 | CSL | Guarded Cubical Type Theory: Path Equality for Guarded Recursion. | Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi |
| 2016 | ESOP | Transfinite Step-Indexing: Decoupling Concrete and Logical Steps. | Kasper Svendsen, Filip Sieczkowski, Lars Birkedal |
| 2016 | FOSSACS | Guarded Dependent Type Theory with Coinductive Types. | Ales Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus Ejlers Mgelberg, Lars Birkedal |
| 2016 | ICFP | Higher-order ghost state. | Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer |
| 2015 | ESOP | A Separation Logic for Fictional Sequential Consistency. | Filip Sieczkowski, Kasper Svendsen, Lars Birkedal, Jean Pichon-Pharabod |
| 2015 | FOSSACS | Step-Indexed Logical Relations for Probability. | Ales Bizjak, Lars Birkedal |
| 2015 | FOSSACS | Programming and Reasoning with Guarded Recursion for Coinductive Types. | Ranald Clouston, Ales Bizjak, Hans Bugge Grathwohl, Lars Birkedal |
| 2015 | ITP | ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages. | Filip Sieczkowski, Ales Bizjak, Lars Birkedal |
| 2015 | POPL | Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. | Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer |
| 2014 | ESOP | Impredicative Concurrent Abstract Predicates. | Kasper Svendsen, Lars Birkedal |
| 2014 | POPL | Modular reasoning about concurrent higher-order imperative programs. | Lars Birkedal |
| 2013 | ECOOP | Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library. | Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson |
| 2013 | ESOP | Modular Reasoning about Separation of Concurrent Data Structures. | Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson |
| 2013 | ICFP | Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. | Aaron Turon, Derek Dreyer, Lars Birkedal |
| 2013 | LICS | Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes. | Lars Birkedal, Rasmus Ejlers Mgelberg |
| 2013 | POPL | Views: compositional reasoning for concurrent programs. | Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, Hongseok Yang |
| 2013 | POPL | Logical relations for fine-grained concurrency. | Aaron Joseph Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, Derek Dreyer |
| 2012 | AiML | First Steps in Synthetic Guarded Domain Theory. | Lars Birkedal |
| 2012 | CSL | A Concurrent Logical Relation. | Lars Birkedal, Filip Sieczkowski, Jacob Thamsborg |
| 2012 | ESOP | Fictional Separation Logic. | Jonas Braband Jensen, Lars Birkedal |
| 2012 | ITP | Charge! - A Framework for Higher-Order Separation Logic in Coq. | Jesper Bengtson, Jonas Braband Jensen, Lars Birkedal |
| 2011 | CSL | Step-Indexed Relational Reasoning for Countable Nondeterminism. | Jan Schwinghammer, Lars Birkedal |
| 2011 | FOSSACS | A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces. | Jan Schwinghammer, Lars Birkedal, Kristian Stvring |
| 2011 | ICFP | A kripke logical relation for effect-based program transformations. | Jacob Thamsborg, Lars Birkedal |
| 2011 | ITP | Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq. | Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski, Lars Birkedal |
| 2011 | LICS | First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees. | Lars Birkedal, Rasmus Ejlers Mgelberg, Jan Schwinghammer, Kristian Stvring |
| 2011 | POPL | Step-indexed kripke models over recursive worlds. | Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Kristian Stvring, Jacob Thamsborg, Hongseok Yang |
| 2010 | ECOOP | Modular verification of linked lists with views via separation logic. | Jonas Braband Jensen, Lars Birkedal, Peter Sestoft |
| 2010 | ECOOP | Verifying Generics and Delegates. | Kasper Svendsen, Lars Birkedal, Matthew J. Parkinson |
| 2010 | FOSSACS | A Semantic Foundation for Hidden State. | Jan Schwinghammer, Hongseok Yang, Lars Birkedal, Franois Pottier, Bernhard Reus |
| 2010 | ICFP | The impact of higher-order state and control effects on local relational reasoning. | Derek Dreyer, Georg Neis, Lars Birkedal |
| 2010 | POPL | A relational modal logic for higher-order stateful ADTs. | Derek Dreyer, Georg Neis, Andreas Rossberg, Lars Birkedal |
| 2009 | CSL | Nested Hoare Triples and Frame Rules for Higher-Order Store. | Jan Schwinghammer, Lars Birkedal, Bernhard Reus, Hongseok Yang |
| 2009 | FOSSACS | Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types. | Lars Birkedal, Kristian Stvring, Jacob Thamsborg |
| 2009 | LICS | Logical Step-Indexed Logical Relations. | Derek Dreyer, Amal Ahmed, Lars Birkedal |
| 2008 | CONCUR | On the Construction of Sorted Reactive Systems. | Lars Birkedal, Sren Debois, Thomas T. Hildebrandt |
| 2008 | ESOP | A Realizability Model for Impredicative Hoare Type Theory. | Rasmus Lerchedahl Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett |
| 2008 | ICALP | A Simple Model of Separation Logic for Higher-Order Store. | Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Hongseok Yang |
| 2008 | ICFP | Ynot: dependent types for imperative programs. | Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, Lars Birkedal |
| 2007 | ESOP | Abstract Predicates and Mutable ADTs in Hoare Type Theory. | Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal |
| 2007 | FOSSACS | Relational Parametricity and Separation Logic. | Lars Birkedal, Hongseok Yang |
| 2006 | APLAS | Relational Reasoning for Recursive Types and References. | Nina Bohr, Lars Birkedal |
| 2006 | CONCUR | Sortings for Reactive Systems. | Lars Birkedal, Sren Debois, Thomas T. Hildebrandt |
| 2006 | FOSSACS | Bigraphical Models of Context-Aware Systems. | Lars Birkedal, Sren Debois, Ebbe Elsborg, Thomas T. Hildebrandt, Henning Niss |
| 2006 | ICFP | Polymorphism and separation in hoare type theory. | Aleksandar Nanevski, Greg Morrisett, Lars Birkedal |
| 2005 | ESOP | BI Hyperdoctrines and Higher-Order Separation Logic. | Bodil Biering, Lars Birkedal, Noah Torp-Smith |
| 2005 | LICS | Semantics of Separation-Logic Typing and Higher-Order Frame Rules. | Lars Birkedal, Noah Torp-Smith, Hongseok Yang |
| 2004 | MMSP | An infrastructure for context dependent mobile multimedia communication. | J. Aa. Serensen, Kre J. Kristoffersen, Andres Cervera, M. Schiortz, Thomas Lynge, Zoltan Safar, Lars Birkedal |
| 2004 | POPL | Local reasoning about a copying garbage collector. | Lars Birkedal, Noah Torp-Smith, John C. Reynolds |
| 2000 | CSL | Continuous Functionals of Dependent Types and Equilogical Spaces. | Andrej Bauer, Lars Birkedal |
| 2000 | LICS | A General Notion of Realizability. | Lars Birkedal |
| 1998 | LICS | Type Theory via Exact Categories. | Lars Birkedal, Aurelio Carboni, Giuseppe Rosolini, Dana S. Scott |
| 1996 | POPL | From Region Inference to von Neumann Machines via Region Representation Inference. | Lars Birkedal, Mads Tofte, Magnus Vejlstrup |
| 1994 | PEPM | Binding-Time Analysis for Standard ML. | Lars Birkedal, Morten Welinder |