Interactive proofs in higher-order concurrent separation logic
From MaRDI portal
Publication:5370856
DOI10.1145/3009837.3009855zbMath1380.68341OpenAlexW2562833768MaRDI QIDQ5370856
Amin Timany, Robbert Krebbers, 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://lirias.kuleuven.be/handle/123456789/553559
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (12)
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems ⋮ On models of higher-order separation logic ⋮ Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms ⋮ VST-Floyd: a separation logic tool to verify correctness of C programs ⋮ Proof tactics for assertions in separation logic ⋮ Unnamed Item ⋮ 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 ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item
Uses Software
This page was built for publication: Interactive proofs in higher-order concurrent separation logic
