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
A grouping.
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).
20 references
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