A relational model of types-and-effects in higher-order concurrent separation logic

DOI10.1145/3009837.3009877zbMath1380.68126OpenAlexW2567502494MaRDI QIDQ5370857

Kasper Svendsen, Morten Krogh-Jespersen, Lars Birkedal

Publication date: 20 October 2017

Published in: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/3009837.3009877

zbMATH Keywords

program transformationseparation logiclogical relationsautomatic parallelisationtype-and-effect system

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Iris from the ground up: A modular foundation for higher-order concurrent separation logic, The Essence of Higher-Order Concurrent Separation Logic, A Higher-Order Logic for Concurrent Termination-Preserving Refinement, Reasoning about block-based cloud storage systems via separation logic, Unnamed Item