Higher-order ghost state
From MaRDI portal
Publication:2985775
DOI10.1145/2951913.2951943zbMath1361.68066OpenAlexW2509578035MaRDI QIDQ2985775
Derek R. Dreyer, Ralf Jung, Robbert Krebbers, Lars Birkedal
Publication date: 10 May 2017
Published in: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/11858/00-001M-0000-002D-067F-8
higher-order logiccompositional verificationseparation logicinteractive theorem provingfine-grained concurrency
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (13)
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems ⋮ Connecting Higher-Order Separation Logic to a First-Order Outside World ⋮ On models of higher-order separation logic ⋮ Ghost signals: verifying termination of busy waiting ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types ⋮ 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 ⋮ Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Linear capabilities for fully abstract compilation of separation-logic-verified code
Uses Software
This page was built for publication: Higher-order ghost state
