On models of higher-order separation logic

DOI10.1016/J.ENTCS.2018.03.016OpenAlexW2800461112WikidataQ113317564 ScholiaQ113317564MaRDI QIDQ2130583

Aleš Bizjak, Lars Birkedal

Publication date: 25 April 2022

Full work available at URL: https://doi.org/10.1016/j.entcs.2018.03.016

zbMATH Keywords

modelseparation logicmodalities

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Iris from the ground up: A modular foundation for higher-order concurrent separation logic

Uses Software

• Unnamed Item
• Toolchain
• Bedrock

Cites Work

• Unnamed Item
• Unnamed Item
• Exponentiable morphisms, partial products and pullback complements
• Iris
• Higher-order ghost state
• The Essence of Higher-Order Concurrent Separation Logic
• A Higher-Order Logic for Concurrent Termination-Preserving Refinement
• Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Adjointness in Foundations
• Syntactic soundness proof of a type-and-capability system with hidden state
• Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency
• Programming Languages and Systems
• Certified assembly programming with embedded code pointers
• Interactive proofs in higher-order concurrent separation logic
• Impredicative Concurrent Abstract Predicates
• Program Logics for Certified Compilers

This page was built for publication: On models of higher-order separation logic