About
Software systems are an integral part of modern society, and software errors and security breaches pose enormous costs and risks. Center for Basic Research in Program Verification develops fundamental mathematically based models and logics for rigorous mathematical reasoning about correctness and security of software systems.
To read more about the research center go to the official center website.
Publications
- Modular Denotational Semantics for Effects with Guarded Interaction Trees
- D. Frumin, A. Timany, and L. Birkedal.
- In Proceedings of POPL 2024.
- Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
- S.O. Gregersen, A. Aguirre, P.G. Haselwarter, J. Tassarotti, and L. Birkedal.
- In Proceedings of POPL 2024.
- An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
- A. Hammon, Z. Liu, T. Perami, P. Sewell, L. Birkedal, and J. Pichon-Pharabod.
- In Proceedings of POPL 2024.
- The Essence of Generalized Algebraic Data Types
- F. Sieczkowski, S. Stepanenko, J. Sterling, and L. Birkedal.
- In Proceedings of POPL 2024.
- Decalf: A Directed, Effectful Cost-Aware Logical Framework
- H. Grodin, Y. Niu, J. Sterling, and R. Harper
- In Proceedings of POPL 2024.
- The Logical Essence of Well-Bracketed Control Flow
- A. Timany, A. Gueneau, and L. Birkedal.
- In Proceedings of POPL 2024.
- Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
- J. Jacobs, J.K. Hinrichsen, and R. Krebbers
- In Proceedings of POPL 2024.
- Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
- A. Timany, S.O. Gregersen, L. Stefanesco, J.K. Hinrichsen, L. Gondelman, A. Nieto, and L. Birkedal.
- In Proceedings of POPL 2024.
- The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
- Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Cătălin Hriţcu, Bas Spitters.
- In CPP 2024: ACM SIGPLAN International Conference on Certified Proofs and Programs.
- Towards univalent reference types: The impact of univalence on denotational semantics
- J. Sterling, D. Gratzer, and L. Birkedal.
- In Proceedings of CSL 2024.
- Melocoton: A Program Logic for Verified Interoperability Between OCaml and C
- A. Gueneau, J. Hostert, S. Spies, M. Sammler, L. Birkedal, and D. Dreyer
- In Proceedings of OOPSLA 2023.
- Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory
- S. Vindum and L. Birkedal
- In Proceedings of OOPSLA 2023.
- Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl)
- J. Jacobs, J.K. Hinrichsen, and R. Krebbers
- In Proceedings of ICFP 2023.
- Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols
- L. Gondelman, J.K. Hinrichsen, A. Timany, and L. Birkedal
- In Proceedings of ICFP 2023.
- Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code
- A.L. Georges, A. Gueneau, T. van Strydonck, A. Timany, A. Trieu, D. Devriese, and L. Birkedal
- Journal of the ACM.
- Under Lock and Key: A Proof System for a Multimodal Logic
- G. A. Kavvos, D. Gratzer
- The Bulletin of Symbolic Logic 2023.
- mitten: A Flexible Multimodal Proof Assistant
- P. Stassen, D. Gratzer, and L. Birkedal
- In Proceedings of Types 2022 (LIPIcs, Volume 269, TYPES 2022).
- Modular Verification of State-Based CRDTs in Separation Logic.
- A. Nieto, A. Daby-Seesaram, L. Gondelman, A. Timany, and L. Birkedal
- In Proceedings of ECOOP 2023.
- A denotationally-based program logic for higher-order store.
- F.L. Aagaard, J. Sterling, and L. Birkedal
- In Proceedings of MFPS 2023.
- What should a generic object be?
- J. Sterling
- Mathematical Structures in Computer Science.
- Iris-Wasm: Robust and Modular Verification of WebAssembly Programs
- X. Rao, A.L. Georges, M. Legoupil, C. Watt, J. Pichon-Pharabod, P. Gardner, and L. Birkedal
- In Proceedings of PLDI 2023.
- VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A.
- Zongyuan Liu, Sergei Stepanenko, Jean Pichon-Pharabod, Amin Timany, Aslan Askarov, Lars Birkedal.
- In Proceedings of PLDI 2023.
- Step-Indexed Logical Relations for Nondeterministic and Probabilistic Choice
- A. Aguirre and L. Birkedal
- In Proceedings of POPL 2023
- Unifying Cubical and Multimodal Type Theory
- Frederik Lerbjerg Aagaard, Magnus Baunsgaard Kristensen, Daniel Gratzer, and Lars Birkedal
- In TYPES 2022: International Conference on Types for Proofs and Programs
- Modular Verification of Op-Based CRDTs in Separation Logic
- A. Nieto, L. Gondelman, A. Reynaud, A.Timany, and L. Birkedal
- In Proceedings of OOPSLA 2022
- Purity of an ST monad: full abstraction by semantically typed back-translation
- K. Jacobs, D. Devriese, and A. Timany
- In Proceedings of OOPSLA 2022
- Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities
- A.L. Georges, A. Trieu, and L. Birkedal
- In Proceedings of OOPSLA 2022
- Weakest preconditions in fibrations
- Alejandro Aguirre, Shin-ya Katsumata, and Satoshi Kura
- Mathematical Constructions in Computer Science 2022
- Later Credits: Resourceful Reasoning for the Later Modality
- S. Spies, L. Gaher, J. Tassarotti, R. Jung, R. Krebbers, L. Birkedal, and D. Dreyer
- In Proceedings of ICFP 2022
- Classifying topoi in synthetic guarded domain theory: the universal property of multi-clock guarded recursion
- Daniele Palombi, Jonathan Sterling
- In MFPS 2022: Mathematical Foundations of Programming Semantics
- Characterizing Functions Mappable Over GADTs.
- Patricia Johann and Pierre Cagne
- In Proceedings of APLAS 2022
- Symbolic Synthesis of Indifferentiability Attacks
- Itsaka Rakotonirina, Miguel Ambrona, Alejandro Aguirre, Gilles Barthe
- In Proceedings of ASIA CCS 2022
- Sheaf semantics of termination-insensitive noninterference
- Jonathan Sterling, Robert Harper
- In FSCD 2022: Formal Structures for Computation and Deduction
- A stratified approach to Löb induction
- Daniel Gratzer, Lars Birkedal
- In FSCD 2022: Formal Structures for Computation and Deduction
- Normalization for multimodal type theory
- Daniel Gratzer
- In LICS 2022: Logic in Computer Science
- A Cubical Language for Bishop Sets
- Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
- Logical Methods in Computer Science 2022
- Modalities and Parametric Adjoints
- Daniel Gratzer, Evan Cavallo, G.A. Kavvos, Adrien Guatto, Lars Birkedal
- Transactions on Computational Logic 2022
- A Cost-Aware Logical Framework
- Y. Niu, J. Sterling, H. Grodin, R. Harper
- In POPL 2022: ACM SIGPLAN Symposium on Principles of Programming Languages
- Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly Library
- S. F. Vindum, D. Frumin, L. Birkedal
- In CPP 2022: ACM SIGPLAN International Conference on Certified Proofs and Programs
- Proving Full-System Security Properties under Multiple Attacker Models on Capability Machines.
- T. Van Strydonck, A.L. Georges, A. Gueneau, A. Trieu, A. Timany, F. Piessens, L. Birkedal, and D. Devriese.
- In CSF 2022: Computer Security Foundations
- Higher-order probabilistic adversarial computations: categorical semantics and program logics
- A. Aguirre, G. Barthe, M. Gaboardi, D. Garg, S. Katsumata, and T. Sato
- In ICFP 2021: ACM SIGPLAN International Conference on Functional Programming
- Theorems for Free from Separation Logic Specifications
- L. Birkedal, T. Dinsdale-Young, A. Gueneau, G. Jaber, K. Svendsen and N. Tzevelekos
- In ICFP 2021: ACM SIGPLAN International Conference on Functional Programming
- Client-Server Sessions in Linear Logic
- Zesen Qian, G. A. Kavvos and Lars Birkedal
- In ICFP 2021: ACM SIGPLAN International Conference on Functional Programming
- Multimodal Dependent Type Theory
- Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal
- In LMCS 2021: Logical Methods in Computer Science 17:3
- 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
- In PLDI 2021: ACM SIGPLAN Conference on Programming Language Design and Implementation
- Toward Complete Stack Safety for Capability Machines
- Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Lars Birkedal
- In PRISC 2021: Principles of Secure Compilation
- [abstract] .pdf
- Cap’ ou pas cap’? Preuve de programmes pour une machine a capacites en presence de code inconnu
- Aïna L. Georges, Armaël Gueneau, Thomas van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal
- In JFLA 2021: Journees Francophones des Langages Applicatifs
- Reasoning About Monotonicity in Separation Logic
- Amin Timany and Lars Birkedal
- In CPP 2021: ACM SIGPLAN International Conference on Certified Proofs and Programs
- Contextual Refinement of the Michael-Scott Queue (Proof Pearl)
- Simon F. Vindum and Lars Birkedal
- In CPP 2021: Certified Proofs and Programs
- 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
- In POPL 2021: ACM SIGPLAN Symposium on Principles of Programming Languages
- Fully Abstract from Static to Gradual
- Koen Jacobs, Amin Timany, and Dominique Devriese.
- In POPL 2021: ACM SIGPLAN Symposium on Principles of Programming Languages
- Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
- Aïna L. Georges, Armaël Gueneau, Thomas van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, Lars Birkedal
- In POPL 2021: ACM SIGPLAN Symposium on Principles of Programming Languages
- Mechanized Logical Relations for Termination-Insensitive Noninterference
- Simon Oddershede Gregersen, Johan Bay, Amin Timany, Lars Birkedal
- In POPL 2021: ACM SIGPLAN Symposium on Principles of Programming Languages
- .pdf Coq development
- StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation using Linear Capabilities
- Lau Skorstengaard, Dominique Devriese, Lars Birkedal
- In JFP 2021: Journal of Functional Programming
- ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
- Dan Frumin, Robbert Krebbers, Lars Birkedal
- In LMCS 2021: Logical Methods in Computer Science 17:3
- 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
- In ICFP 2020: ACM SIGPLAN International Conference on Functional Programming
- .pdf website
- Compositional Non-Interference for Fine-Grained Concurrent Programs
- Dan Frumin, Robbert Krebbers, Lars Birkedal
- In S&P 2021: Security and Privacy (Oakland)
- .pdf Coq development
- Multimodal Dependent Type Theory
- Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal
- In LICS 2020: Logic in Computer Science
- Dual-Context Calculi for Modal Logic
- G. A. Kavvos
- In LMCS 2020: Logical Methods in Computer Science
- Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems
- Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, Lars Birkedal
- In ESOP 2020: European Symposium on Programming
- .pdf technical appendix Coq development
- Mechanized Reasoning about a Capability Machine
- Aïna Linn Georges, Alix Trieu, Lars Birkedal
- In PRISC 2020: Principles of Secure Compilation
- [abstract] .pdf
- Cubical Syntax for Reflection-Free Extensional Equality
- Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
- In FSCD 2019: Formal Structures for Computation and Deduction,
- Implementing a Modal Dependent Type Theory
- Daniel Gratzer, Jonathan Sterling, Lars Birkedal
- In ICFP 2019: ACM SIGPLAN International Conference on Functional Programming
- Mechanized Relational Verification of Concurrent Programs with Continuations
- Amin Timany and Lars Birkedal
- In ICFP 2019: ACM SIGPLAN International Conference on Functional Programming
- Modal Dependent Type Theory and Dependent Right Adjoints
- Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Møgelberg, Andrew M. Pitts, Bas Spitters
- In MSCS 2019: Mathematical Structures in Computer Science
- Iron: Managing Obligations in Higher-Order Concurrent Separation Logic
- Aleš Bizjak, Daniel Gratzer, Robbert Krebbers, Lars Birkedal
- In POPL 2019: ACM SIGPLAN Symposium on Principles of Programming Languages
- StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation using Linear Capabilities
- Lau Skorstengaard, Dominique Devriese, Lars Birkedal
- In POPL 2019: ACM SIGPLAN Symposium on Principles of Programming Languages
- Guarded Cubical Type Theory
- Lars Birkedal, Aleš Bizjak, Ranald Clouston, Hans B. Grathwohl, Bas Spitters, Andrea Vezzosi
- In JAR 2019: Journal of Automated Reasoning
- Reasoning about a Capability Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management
- Lau Skorstengaard, Dominique Devriese, Lars Birkedal
- In TOPLAS 2019: ACM Transactions on Programming Languages and Systems
Draft papers
- A Logical Approach to Type Soundness
- Amin Timany, Robbert Krebbers, Derek Dreyer, and Lars Birkedal
- Submitted for publication
- [preprint] pdf
- Controlling unfolding in type theory
- D. Gratzer, J. Sterling, C. Angiuli, T. Coquand, L. Birkedal
- Submitted for publication
- [preprint] pdf
- Denotational semantics of general store and polymorphism
- J. Sterling, D. Gratzer, L. Birkedal
- Submitted for publication
- [preprint] pdf
- Strict universes for Grothendieck topoi
- D. Gratzer, M. Shulman, J. Sterling
- Submitted for publication
- [preprint] pdf
- Syntactic categories for dependent type theory: sketching and adequacy
- Daniel Gratzer, Jonathan Sterling
- [preprint] pdf
