Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency

DOI10.1145/2500365.2500600zbMath1323.68386OpenAlexW2028861803MaRDI QIDQ5244818

Aaron Joseph Turon, Derek R. Dreyer, Lars Birkedal

Publication date: 30 March 2015

Published in: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

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

zbMATH Keywords

separation logichigher-order functionsKripke logical relationsfine-grained concurrencycontextual refinement

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (22)

Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems ⋮ Abstract local reasoning for concurrent libraries: mind the gap ⋮ On models of higher-order separation logic ⋮ Caper ⋮ Verifying Concurrent Graph Algorithms ⋮ A perspective on specifying and verifying concurrent modules ⋮ Stateful applied pi calculus: observational equivalence and labelled bisimilarity ⋮ Balancing expressiveness in formal approaches to concurrency ⋮ Higher-order linearisability ⋮ Concise outlines for a complex logic: a proof outline checker for TaDA ⋮ Steps in modular specifications for concurrent modules (invited tutorial paper) ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic ⋮ Proving Linearizability Using Partial Orders ⋮ The Essence of Higher-Order Concurrent Separation Logic ⋮ A Higher-Order Logic for Concurrent Termination-Preserving Refinement ⋮ Abstract Specifications for Concurrent Maps ⋮ Unnamed Item ⋮ Modular Termination Verification for Non-blocking Concurrency ⋮ Transfinite Step-Indexing: Decoupling Concrete and Logical Steps ⋮ Unnamed Item ⋮ Contextual Approximation and Higher-Order Procedures ⋮ Unnamed Item

This page was built for publication: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency