Ribbon proofs for separation logic

DOI10.1007/978-3-642-37036-6_12MaRDI QIDQ5326286zbMATH OpenOpenAlexFDO

Authors John Wickerson, Mike Dodds, Matthew J. Parkinson

Publication date 5 August 2013

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-37036-6_12

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Recommendations

• Ribbon proofs
• Computer Science Logic
• Separation logic adapted for proofs by rewriting
• A proof system for separation logic with magic wand
• Program Verification with Separation Logic

Cited in

(4)

• Ribbon proofs
• Semi-intelligible Isar proofs from machine-generated proofs
• Shaded tangles for the design and verification of quantum programs (extended abstract)
• Shaded tangles for the design and verification of quantum circuits

Describes a project that uses

Uses Software

• Isabelle

This page was built for publication: Ribbon proofs for separation logic

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