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 verificationfine-grained concurrencyhigher-order logicinteractive theorem provingseparation logic

Mathematics Subject Classification ID

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

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

(19)

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

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)