Labelled cyclic proofs for separation logic

DOI10.1093/LOGCOM/EXAB017MaRDI QIDQ3382810zbMATH OpenOpenAlexWikidataFDO

Authors Didier Galmiche, Daniel Méry

Publication date 22 September 2021

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/logcom/exab017

Mathematics Subject Classification ID

Mathematical logic and foundations (03-XX) Computer science (68-XX)

Recommendations

• Completeness of cyclic proofs for symbolic heaps with inductive definitions
• Automated cyclic entailment proofs in separation logic
• Cyclic proofs of program termination in separation logic
• A proof system for separation logic with magic wand
• Tableaux and resource graphs for separation logic

Cited in

(5)

• Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps
• Procedural representation of CIC proof terms
• A proof procedure for separation logic with inductive definitions and data
• Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions
• Completeness of cyclic proofs for symbolic heaps with inductive definitions

This page was built for publication: Labelled cyclic proofs for separation logic

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