Higher-order ghost state

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

zbMATH Keywords

higher-order logiccompositional verificationseparation logicinteractive theorem provingfine-grained concurrency

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Functional programming and lambda calculus (68N18) 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

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

• Coq