Ribbon proofs for separation logic

DOI10.1007/978-3-642-37036-6_12zbMATH Open1381.68065OpenAlexW1484252365MaRDI QIDQ5326286FDOQ5326286

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

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

Mathematics Subject Classification ID

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

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

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)