Lars Birkedal

6 references under this name, matched as it is written. Somebody else may write under it too, and the same person may appear here spelled another way.

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

The model-theoretic side of separation logic -- what the logic means rather than what it proves: relational parametricity, models of higher-order separation logic, and design patterns applying it. Two records carry furthest, both on Iris: the framework itself in 'Iris from the ground up', and the proof mode that made it usable inside Coq. A sixth, 'Views', puts several concurrent logics on one footing.

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
Interactive proofs in higher-order concurrent separation logic
Robbert Krebbers and others (2017) · 44th ACM 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
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 (2007) · 10th International Conference on Foundations of Software Science and Computational Structures (FoSSaCS) · Springer