Lars Birkedal

Research output

Research output per year 1994 2004 2006 2007 2008 2009 2010 2011 2012 2013 2015 2016 2018 2019 2020 2021 2022 2023 2024 2025

• 85 Article in proceedings
• 82 Journal article
• 17 Conference article
• 8 Working paper
• 19 More
  • 7 Anthology
  • 3 Conference abstract for conference
  • 2 Book chapter
  • 2 Paper
  • 1 Book
  • 1 Report
  • 1 Editorial
  • 1 Literature review
  • 1 Net publication - Internet publication

Research output per year

Research output per year

Search results

• 2025

  Approximate Relational Reasoning for Higher-Order Probabilistic Programs

  Haselwarter, P. G., Li, K. H., Aguirre, A., Gregersen, S. O., Tassarotti, J. & Birkedal, L., 7 Jan 2025, In: Proceedings of the ACM on Programming Languages . 9, POPL, p. 1196-1226 31 p., 41.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  • Approximate Equivalence 100%
  • Probabilistic Sampling 50%
  • Provable Correctness 33%
  • Relational Logic 33%
  • Relational Rules 33%

• Context-Dependent Effects in Guarded Interaction Trees

  Stepanenko, S., Nardino, E., Frumin, D., Timany, A. & Birkedal, L., 2025, Programming Languages and Systems - 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings. Vafeiadis, V. (ed.). Springer, Vol. Part II. p. 286-313 28 p. (Lecture Notes in Computer Science, Vol. 15695).

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  Open Access

  • Context Dependent 100%
  • Interaction Trees 100%
  • Logic Programming 80%
  • Programming Language 60%
  • Denotational Semantics 40%

• Idempotent Resources in Separation Logic: The Heart of core in Iris

  Gratzer, D., Møller, M. A. & Birkedal, L., 2025, Foundations of Software Science and Computation Structures - 28th International Conference, FoSSaCS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software: ETAPS 2025, Proceedings. Abdulla, P. A. & Kesner, D. (eds.). Springer Science and Business Media Deutschland GmbH, p. 45-66 22 p. (Lecture Notes in Computer Science, Vol. 15691 LNCS).

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  Open Access

  • Formalization 100%
  • Idempotent Element 100%
  • Universal Property 33%
  • Core Operator 33%
  • Partially Commutative Monoid 33%

• Modelling Recursion and Probabilistic Choice in Guarded Type Theory

  Stassen, P., Møgelberg, R. E., Zwart, M. A., Aguirre, A. & Birkedal, L., 9 Jan 2025, In: Proceedings of the ACM on Programming Languages . 9, POPL, p. 1417-1445 29 p., 48.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  • Probabilistic Choice 100%
  • Programming Language 66%
  • Constructive Type 66%
  • Constructive Type Theory 50%
  • Operational Semantics 33%
  1 Citation (Scopus)

• The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic

  Vindum, S. F., Georges, A. L. & Birkedal, L., Jan 2025, Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with: POPL 2025. Stark, K., Timany, A., Blazy, S. & Tabareau, N. (eds.). Association for Computing Machinery, Inc., p. 83-97 15 p.

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  • Next-Gen 100%
  • Reasoning Rules 50%
  • Stack Allocation 33%
  • Program Reasoning 33%
  • Ghost States 16%
• 2024

  Almost-Sure Termination by Guarded Refinement

  Gregersen, S. O., Aguirre, A., Haselwarter, P. G., Tassarotti, J. & Birkedal, L., Aug 2024, In: Proceedings of the ACM on Programming Languages . 8, ICFP, p. 203-233 31 p., 243.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  • Syntactics 100%
  • Proving Termination 100%
  • Logic Programming 100%
  • Caliper 80%
  • Recursion Pattern 40%
  2 Citations (Scopus)

• A Logical Approach to Type Soundness

  Timany, A., Krebbers, R., Dreyer, D. & Birkedal, L., Nov 2024, In: Journal of the ACM. 71, 6, 40.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  • Type Soundness 100%
  • Logical Approach 100%
  • Semantic Types 27%
  • Logic Styles 18%
  • Language Features 9%
  8 Citations (Scopus)

• An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic

  Hammond, A., Liu, Z., Pérami, T., Sewell, P., Birkedal, L. & Pichon-Pharabod, J., 5 Jan 2024, In: Proceedings of the ACM on Programming Languages . 8, p. 604-637 34 p., 21.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  • Memory Model 100%
  • Computer Programming 100%
  • Concurrency 66%
  • Systems Performance 33%
  • Syntactics 33%
  1 Citation (Scopus)

• Asynchronous Probabilistic Couplings in Higher-Order Separation Logic

  Gregersen, S. O., Aguirre, A., Haselwarter, P. G., Tassarotti, J. & Birkedal, L., Jan 2024, In: Proceedings of the ACM on Programming Languages . 8, POPL, 26.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  • Logic Programming 100%
  • And-States 50%
  • Logical Relation 50%
  • Probabilistic Choice 50%
  • Case Study 50%
  7 Citations (Scopus)

• Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code

  Georges, A. L., Guéneau, A., Van Strydonck, T., Timany, A., Trieu, A., Devriese, D. & Birkedal, L., 12 Feb 2024, In: Journal of the ACM. 71, 1, 59 p., 3.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  • Logical Relation 100%
  • Program Verification 100%
  • Logic Programming 100%
  • Formal Verification 33%
  • High-Level Language 33%
  2 Citations (Scopus)

• Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs

  Aguirre, A., Haselwarter, P. G., De Medeiros, M., Li, K. H., Gregersen, S. O., Tassarotti, J. & Birkedal, L., Aug 2024, In: Proceedings of the ACM on Programming Languages . 8, 246.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  • Error Bound 100%
  • Separation Logic 100%
  • Collision Probability 100%
  • Error Probability Bounds 50%
  • Rejection Sampling 25%
  3 Citations (Scopus)

• Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly

  Legoupil, M., Rousseau, J., Georges, A. L., Pichon-Pharabod, J. & Birkedal, L., Oct 2024, In: Proceedings of the ACM on Programming Languages . 8, OOPSLA2, 282.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  • Security Invariant 100%
  • Memory Safe 100%
  • WebAssembly 100%
  • Robust Capability 40%
  • Module System 40%
  1 Citation (Scopus)

• Modular Denotational Semantics for Effects with Guarded Interaction Trees

  Frumin, D., Timany, A. & Birkedal, L., Jan 2024, In: Proceedings of the ACM on Programming Languages . 8, POPL, 12.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  • Denotational Semantics 100%
  • Domain Theory 100%
  • Soundness 100%
  • Logical Relation 100%
  • Interoperability 100%
  6 Citations (Scopus)

• Tachis: Higher-Order Separation Logic with Credits for Expected Costs

  Haselwarter, P. G., Li, K. H. E. I., Medeiros, M. D. E., Gregersen, S. O., Aguirre, A., Tassarotti, J. & Birkedal, L., 8 Oct 2024, In: Proceedings of the ACM on Programming Languages . 8, OOPSLA2, p. 1189 - 1218 313.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  • Data Structure 100%
  • Quicksort 50%
  • Hash Table 50%
  • Probabilistic Cost Analysis 40%
  • Cost Model 20%
  1 Citation (Scopus)

• The Essence of Generalized Algebraic Data Types

  Sieczkowski, F., Stepanenko, S., Sterling, J. & Birkedal, L., Jan 2024, In: Proceedings of the ACM on Programming Languages . 8, POPL, p. 695-723 29 p.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  • Data Type 100%
  • Calculus 100%
  • Pattern Matching 25%
  • Relational Database 25%
  • lambda-calculus 25%
  1 Citation (Scopus)

• The Logical Essence of Well-Bracketed Control Flow

  Timany, A., Guéneau, A. & Birkedal, L., Jan 2024, In: Proceedings of the ACM on Programming Languages . 8, POPL, p. 575-603 29 p.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  • Control Flow 100%
  • Logic Programming 66%
  • Relational Database 33%
  • Transition System 33%
  • Security Properties 33%
  1 Citation (Scopus)

• Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics

  Sterling, J., Gratzer, D. & Birkedal, L., Feb 2024, 32nd EACSL Annual Conference on Computer Science Logic, CSL 2024. Murano, A. & Silva, A. (eds.). Dagstuhl Publishing, 47. (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 288).

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  Open Access

  • Denotational Semantics 100%
  • Domain Theory 33%
  1 Citation (Scopus)

• Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement

  Timany, A., Gregersen, S. O., Stefanesco, L., Hinrichsen, J. K., Gondelman, L., Nieto, A. & Birkedal, L., 5 Jan 2024, In: Proceedings of the ACM on Programming Languages . 8, 9.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  • Liveness Property 100%
  • Concurrent Program 100%
  • Refinement Relation 100%
  • Distributed Systems 50%
  • Concurrent Language 50%
  3 Citations (Scopus)
• 2023

  A denotationally-based program logic for higher-order store

  Aagaard, F. L., Sterling, J. & Birkedal, L., 2023, In: Electronic Notes in Theorical Informatics and Computer Science. 3

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Conference article › Research › peer-review

  Open Access

  File
  4 Downloads (Pure)

• Iris-Wasm: Robust and Modular Verification of WebAssembly Programs

  Rao, X., Georges, A. L., Legoupil, M., Watt, C., Pichon-Pharabod, J., Gardner, P. & Birkedal, L., Jun 2023, In: Proceedings of the ACM on Programming Languages . 7, 151.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  File

  • WebAssembly 100%
  9 Citations (Scopus)

  2 Downloads (Pure)

• Melocoton: A Program Logic for Verified Interoperability Between OCaml and C

  Guéneau, A., Hostert, J., Spies, S., Sammler, M., Birkedal, L. & Dreyer, D., Oct 2023, In: Proceedings of the ACM on Programming Languages . 7, OOPSLA2, p. 716-744 29 p., 247.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  File

  • Language Program 100%
  7 Citations (Scopus)

  1 Downloads (Pure)

• mitten: A Flexible Multimodal Proof Assistant

  Stassen, P. J. A., Gratzer, D. & Birkedal, L., Aug 2023, 28th International Conference on Types for Proofs and Programs. Kesner, D. & Pedrot, P.-M. (eds.). Nantes: Dagstuhl Publishing, 6. (Leibniz International Proceedings in Informatics, Vol. 269).

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  Open Access

  • Type Checking 100%
  • Type Checking Algorithm 100%
  • Type Constructor 100%
  5 Citations (Scopus)

• Modular Verification of State-Based CRDTs in Separation Logic

  Nieto, A., Daby-Seesaram, A., Gondelman, L., Timany, A. & Birkedal, L., Jul 2023, 37th European Conference on Object-Oriented Programming, ECOOP 2023. Ali, K. & Salvaneschi, G. (eds.). Dagstuhl Publishing, 22. (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 263).

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  Open Access

  • And-States 100%
  • Subclasses 100%
  • Distributed Data Structure 100%
  • State Building 100%
  • Abstract Data Type 100%
  2 Citations (Scopus)

• Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory

  Vindum, S. F. & Birkedal, L., Oct 2023, In: Proceedings of the ACM on Programming Languages . 7, OOPSLA2, p. 632-657 26 p., 244.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  File

  • Persistent Memory 100%
  • Data Structure 50%
  • Emerging Technology 25%
  • Memory Model 25%
  • Main Memory 25%
  2 Citations (Scopus)

  1 Downloads (Pure)

• Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice

  Aguirre, A. & Birkedal, L., 9 Jan 2023, In: Proceedings of the ACM on Programming Languages . 7, p. 33-60 28 p., 2.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  File

  • Logical Relation 100%
  • Probabilistic Choice 100%
  • Nondeterminism 100%
  • Parametric Polymorphism 50%
  • Equational Theory 50%
  9 Citations (Scopus)

  2 Downloads (Pure)

• Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols

  Gondelman, L., Hinrichsen, J. K., Pereira, M., Timany, A. & Birkedal, L., Aug 2023, In: Proceedings of the ACM on Programming Languages . 7, ICFP, p. 847-877 31 p., 217.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  File

  • Network Component 100%
  • Reliable Communication 100%
  • Client Server 50%
  • Existing Protocol 50%
  • Formal Reasoning 50%
  5 Citations (Scopus)

  1 Downloads (Pure)

• VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A

  Liu, Z., Stepanenko, S., Pichon-Pharabod, J., Timany, A., Askarov, A. & Birkedal, L., Jun 2023, In: Proceedings of the ACM on Programming Languages . 7, p. 1438-1462

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  File

  • Virtual Machine 100%
  • Hypervisor 57%
  • Operating Systems 14%
  • Execution Model 14%
  • Security Component 14%
  1 Citation (Scopus)

  2 Downloads (Pure)
• 2022

  A Stratified Approach to Löb Induction

  Gratzer, D. & Birkedal, L., Jun 2022, 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022. Felty, A. P. (ed.). Dagstuhl Publishing, 23. (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 228).

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  Open Access

  • Type Checking 100%
  • Metatheory 50%
  • Propositional Rule 50%
  • Definitional Equality 50%
  6 Citations (Scopus)

• Later credits: resourceful reasoning for the later modality

  Spies, S., Gäher, L., Tassarotti, J., Jung, R., Krebbers, R., Birkedal, L. & Dreyer, D., 29 Aug 2022, In: Proceedings of the ACM on Programming Languages . 6, ICFP, 100.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  File

  • Logical Relation 100%
  • Logical Separation 100%
  13 Citations (Scopus)

  6 Downloads (Pure)

• Le temps des cerises: Efficient temporal stack safety on capability machines using directed capabilities

  Georges, A. L., Trieu, A. & Birkedal, L., Apr 2022, In: Proceedings of the ACM on Programming Languages . 6, OOPSLA1, 30 p., 74.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  File

  • Logical Relation 100%
  • Calling Convention 100%
  • Control Flow 33%
  • Concrete Example 33%
  9 Citations (Scopus)

  6 Downloads (Pure)

• Mechanized Verification of a Fine-Grained Concurrent Queue from Meta s Folly Library

  Vindum, S. F., Frumin, D. & Birkedal, L., Jan 2022, CPP 2022 : Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022. Popescu, A. & Zdancewic, S. (eds.). Association for Computing Machinery, p. 100-115 (CPP 2022 - Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs).

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  Open Access

  • Machine Learning 100%
  • Formal Verification 100%
  • Formal Specification 100%
  • Infrastructure Component 100%
  • Logic Programming 100%
  6 Citations (Scopus)

• Modalities and Parametric Adjoints

  Gratzer, D., Cavallo, E., Kavvos, G. A., Guatto, A. & Birkedal, L., Jul 2022, In: ACM Transactions on Computational Logic. 23, 3, 18.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  • Classes 100%
  • Contexts 100%
  • Recursion 100%
  5 Citations (Scopus)

• Modular verification of op-based CRDTs in separation logic

  Nieto, A., Gondelman, L., Reynaud, A., Timany, A. & Birkedal, L., 31 Oct 2022, In: Proceedings of the ACM on Programming Languages . 6, OOPSLA2, p. 1788-1816 29 p., 188.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  File

  • Data Type 100%
  • And-States 20%
  • Data Structure 20%
  • Concurrency Control 20%
  • Correctness Proofs 20%
  12 Citations (Scopus)

  24 Downloads (Pure)

• Proving full-system security properties under multiple attacker models on capability machines

  Strydonck, T. V., Georges, A. L., Guéneau, A., Trieu, A., Timany, A., Piessens, F., Birkedal, L. & Devriese, D., Oct 2022, Proceedings - 2022 IEEE 35th Computer Security Foundations Symposium, CSF 2022. IEEE, p. 80-95 16 p.

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  • External Effects 100%
  4 Citations (Scopus)

• Unifying Cubical and Multimodal Type Theory

  Aagaard, F. L., Kristensen, M., Gratzer, D. & Birkedal, L., 2022. 3 p.

  Research output: Contribution to conference › Conference abstract for conference › Research › peer-review

  Open Access
• 2021

  Cap’ ou pas cap’ ?: Preuve de programmes pour une machine à capacités en présence de code inconnu

  Georges, A. L., Guéneau, A., Van Strydonck, T., Timany, A., Trieu, A., Devriese, D. & Birkedal, L., 7 Apr 2021, Journées Francophones des Langages Applicatifs 2021. Institut de Recherche en Informatique Fondamentale

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  Open Access

• Cap’ ou pas cap’ ? Preuve de programmes pour une machine à capacités en présence de code inconnu

  Translated title of the contribution: To cap or not to cap? Proof of programs for a capacity machine in the presence of unknown codeGeorges, A. L., Guéneau, A., Van Strydonck, T., Timany, A., Trieu, A., Devriese, D. & Birkedal, L., 2021, p. 157-173. 17 p.

  Research output: Contribution to conference › Paper › Research › peer-review

  2 Citations (Scopus)

• Client-server sessions in linear logic

  Qian, Z., Kavvos, G. A. & Birkedal, L., Aug 2021, In: Proceedings of the ACM on Programming Languages . 5, ICFP, 31 p., 62.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  File

  • Client Server 100%
  • Linear Logic 100%
  • Structural Rule 33%
  • Programming Language 33%
  • Arbitrary Number 33%
  16 Citations (Scopus)

  23 Downloads (Pure)

• Compositional non-interference for fine-grained concurrent programs

  Frumin, D., Krebbers, R. & Birkedal, L., May 2021, 2021 IEEE Symposium on Security and Privacy (SP). IEEE, p. 1416-1433 18 p.

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  • Type Systems 100%
  • Concurrent Program 100%
  • Logic Programming 60%
  • Type Checking 40%
  • Logical Relation 20%
  11 Citations (Scopus)

• Contextual refinement of the Michael-Scott queue (proof pearl)

  Vindum, S. F. & Birkedal, L., Jan 2021, CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs. Hriţcu, C. & Popescu, A. (eds.). New York: Association for Computing Machinery, p. 76-90 15 p.

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  Open Access

  • Refines 100%
  • Formalization 50%
  14 Citations (Scopus)

• Distributed causal memory: Modular specification and verification in higher-order distributed separation logic

  Gondelman, L., Gregersen, S. O., Nieto, A., Timany, A. & Birkedal, L., Jan 2021, In: Proceedings of the ACM on Programming Languages . 5, POPL, 29 p., 42.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  File

  • Distributed Databases 100%
  • Machine Learning 33%
  • Distributed Systems 33%
  • Library Manager 33%
  • Programming Language 33%
  10 Citations (Scopus)

  35 Downloads (Pure)

• Efficient and provable local capability revocation using uninitialized capabilities

  Georges, A. L., Guéneau, A., Van Strydonck, T., Timany, A., Trieu, A., Huyghebaert, S., Devriese, D. & Birkedal, L., Jan 2021, In: Proceedings of the ACM on Programming Languages . 5, POPL, 30 p., 6.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  File

  • Logic Programming 100%
  • Reasoning about Programs 50%
  • Restricted Form 50%
  • Calling Convention 50%
  20 Citations (Scopus)

  17 Downloads (Pure)

• Mechanized logical relations for termination-insensitive noninterference

  Gregersen, S. O., Bay, J., Timany, A. & Birkedal, L., Jan 2021, In: Proceedings of the ACM on Programming Languages . 5, POPL, 10.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  File

  • Logical Relation 100%
  • Type Systems 100%
  • Information Flow Control 50%
  • Weakest Precondition 50%
  • Logic Programming 50%
  9 Citations (Scopus)

  20 Downloads (Pure)

• Multimodal Dependent Type Theory

  Gratzer, D., Kavvos, G. A., Nuyts, A. & Birkedal, L., Jul 2021, In: Logical Methods in Computer Science. 17, 3, 67 p., 11.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  • Multi-modal 100%
  • Modal 100%
  • Type Theory 100%
  • Dependent Type 100%
  • Metatheory 100%
  23 Citations (Scopus)

• Reasoning about monotonicity in separation logic

  Timany, A. & Birkedal, L., Jan 2021, Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’21). New York: Association for Computing Machinery, p. 91-104 14 p.

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  Open Access

  • Preorder 100%
  • Logic Programming 100%
  • Resource Model 100%
  • Monoids 80%
  10 Citations (Scopus)

• ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity

  Frumin, D., Krebbers, R. & Birkedal, L., Jul 2021, In: Logical Methods in Computer Science. 17, 3, 59 p., 9.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  • Concurrency 100%
  • And-States 33%
  • Soundness 33%
  • Symbolic Execution 33%
  • Structural Rule 33%
  14 Citations (Scopus)

• StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities

  Skorstensgaard, L., Devriese, D. & Birkedal, L., 15 Apr 2021, In: Journal of Functional Programming. 31, 75 p., e9.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  • Control Flow 100%
  • Calling Convention 100%
  5 Citations (Scopus)

• Theorems for free from separation logic specifications

  Birkedal, L., Dinsdale-Young, T., Guéneau, A., Jaber, G., Svendsen, K. & Tzevelekos, N., Aug 2021, In: Proceedings of the ACM on Programming Languages . 5, ICFP, 81.

  Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

  Open Access

  File
  15 Citations (Scopus)

  20 Downloads (Pure)

• Transfinite Iris: Resolving an existential dilemma of step-indexed separation logic

  Spies, S., Gäher, L., Gratzer, D., Tassarotti, J., Krebbers, R., Dreyer, D. & Birkedal, L., Jun 2021, PLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. Freund, S. N. & Yahav, E. (eds.). New York: Association for Computing Machinery, p. 80-95 16 p.

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  Open Access

  • Liveness Property 100%
  • Liveness 50%
  • Proving Termination 50%
  20 Citations (Scopus)
• 2020

  Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems

  Krogh-Jespersen, M., Timany, A., Ohlenbusch, M. E., Gregersen, S. O. & Birkedal, L., 1 Jan 2020, Programming Languages and Systems- 29th European Symposium on Programming ESOP 2020 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings. Müller, P. (ed.). Springer, p. 336-365 30 p. (Lecture Notes in Computer Science, Vol. 12075).

  Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

  Open Access

  File

  • Distributed Systems 100%
  • Concurrent System 25%
  • Two-Phase Commit 25%
  • Phase Commit Protocol 25%
  • Multiple Server 25%
  23 Citations (Scopus)

  61 Downloads (Pure)