This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.

Lars Birkedal

Lars Birkedal: the model theory of separation logic - relational parametricity, models of higher-order separation logic, design patterns, Views, and Iris (the framework and its Coq proof mode).

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

Aïna Linn Georges and others (2022) · Proceedings of the ACM on Programming Languages · Association for Computing Machinery

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

Thomas Van Strydonck and others (2022) · Proceedings - Computer Security Foundations Workshop/Proceedings · Institute of Electrical and Electronics Engineers

Efficient and provable local capability revocation using uninitialized capabilities

Aïna Linn Georges and others (2021) · Proceedings of the ACM on Programming Languages · Association for Computing Machinery

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

Lau Skorstengaard and others (2021) · Journal of Functional Programming · Cambridge University Press

Reasoning about a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management

Lau Skorstengaard and others (2020) · ACM Transactions on Programming Languages and Systems · Association for Computing Machinery

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

Lau Skorstengaard and others (2019) · Proceedings of the ACM on Programming Languages · Association for Computing Machinery

On models of higher-order separation logic

Aleš Bizjak and others (2018) · Electronic Notes in Theoretical Computer Science

Iris from the ground up: A modular foundation for higher-order concurrent separation logic

Ralf Jung and others (2018) · Journal of Functional Programming · Cambridge University Press

Reasoning about a machine with local capabilities: Provably safe stack and return pointer management

Lau Skorstengaard and others (2018) · Springer International Publishing

Interactive proofs in higher-order concurrent separation logic

Robbert Krebbers and others (2017) · 44th ACM Symposium on Principles of Programming Languages (POPL)

Reasoning about Object Capabilities with Logical Relations and Effect Parametricity

Dominique Devriese and others (2016) · IEEE European Symposium on Security and Privacy

Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning

Ralf Jung and others (2015) · ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)

Views: compositional reasoning for concurrent programs

Thomas Dinsdale-Young and others (2013) · 40th ACM Symposium on Principles of Programming Languages (POPL) · Association for Computing Machinery

Charge!

Jesper Bengtson and others (2012) · Lecture notes in computer science · Springer Science+Business Media

Design patterns in separation logic

Neelakantan R. Krishnaswami and others (2009) · 4th International Workshop on Types in Language Design and Implementation · Association for Computing Machinery

Relational Parametricity and Separation Logic

Lars Birkedal and others (2008) · Logical Methods in Computer Science · Centre pour la Communication Scientifique Directe (CCSD)

Relational parametricity and separation logic

Lars Birkedal and others (2007) · 10th International Conference on Foundations of Software Science and Computational Structures (FoSSaCS) · Springer

Polymorphism and separation in hoare type theory

Aleksandar Nanevski and others (2006) · ACM SIGPLAN International Conference on Functional Programming (ICFP)

BI Hyperdoctrines and Higher-Order Separation Logic

Bodil Biering and others (2005) · Lecture notes in computer science · Springer Science+Business Media

Local reasoning about a copying garbage collector

Lars Birkedal and others (2004) · ACM SIGPLAN Notices · Association for Computing Machinery