Higher-order ghost state

DOI10.1145/2951913.2951943MaRDI QIDQ2985775zbMATH OpenOpenAlexFDO

Authors Ralf Jung, Robbert Krebbers, Derek Dreyer, 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

compositional verificationseparation logichigher-order logicinteractive theorem provingfine-grained concurrency

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• The essence of higher-order concurrent separation logic
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Interactive proofs in higher-order concurrent separation logic
• Revisiting concurrent separation logic
• Iris: monoids and invariants as an orthogonal basis for concurrent reasoning

Cited in

(16)

• Ghost signals: verifying termination of busy waiting
• Connecting higher-order separation logic to a first-order outside world
• scientific article; zbMATH DE number 7566072 (Why is no real title available?)
• On models of higher-order separation logic
• Linear capabilities for fully abstract compilation of separation-logic-verified code
• The essence of higher-order concurrent separation logic
• A higher-order logic for concurrent termination-preserving refinement
• A logical approach to type soundness
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
• scientific article; zbMATH DE number 7407781 (Why is no real title available?)
• Modular verification of intrusive list and tree data structures in separation logic
• An algebraic glimpse at bunched implications and separation logic
• Idempotent resources in separation logic. The heart of \texttt{core} in Iris
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• Aneris: a mechanised logic for modular reasoning about distributed systems

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Higher-order ghost state

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2985775)