Ribbon proofs for separation logic

John Wickerson; Mike Dodds; Matthew J. Parkinson

doi:10.1007/978-3-642-37036-6_12

Ribbon proofs for separation logic

John Wickerson, Mike Dodds, Matthew J. Parkinson

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

We present ribbon proofs, a diagrammatic system for proving program correctness based on separation logic. Ribbon proofs emphasise the structure of a proof, so are intelligible and pedagogical. Because they contain less redundancy than proof outlines, and allow each proof step to be checked locally, they may be more scalable. Where proof outlines are cumbersome to modify, ribbon proofs can be visually manoeuvred to yield proofs of variant programs. This paper introduces the ribbon proof system, proves its soundness and completeness, and outlines a prototype tool for validating the diagrams in Isabelle.

Original language	English
Title of host publication	Programming Languages and Systems
Subtitle of host publication	ESOP'13 Proceedings of the 22nd European conference on Programming Languages and Systems
Publisher	ACM
Pages	189-208
Number of pages	10
Volume	7792 LNCS
ISBN (Print)	978-3-642-37035-9
DOIs	https://doi.org/10.1007/978-3-642-37036-6_12
Publication status	Published - 16 Mar 2013
Event	22nd European conference on Programming Languages and Systems (ESOP 2013) - Rome, Italy Duration: 16 Mar 2013 → 24 Mar 2013

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	7792
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	22nd European conference on Programming Languages and Systems (ESOP 2013)
Country/Territory	Italy
City	Rome
Period	16/03/13 → 24/03/13

Access to Document

10.1007/978-3-642-37036-6_12

http://dl.acm.org/citation.cfm?id=2450268.2450284

Cite this

@inproceedings{7e9ba5a635e54bdf8e8ae11d38404b44,

title = "Ribbon proofs for separation logic",

abstract = "We present ribbon proofs, a diagrammatic system for proving program correctness based on separation logic. Ribbon proofs emphasise the structure of a proof, so are intelligible and pedagogical. Because they contain less redundancy than proof outlines, and allow each proof step to be checked locally, they may be more scalable. Where proof outlines are cumbersome to modify, ribbon proofs can be visually manoeuvred to yield proofs of variant programs. This paper introduces the ribbon proof system, proves its soundness and completeness, and outlines a prototype tool for validating the diagrams in Isabelle.",

author = "John Wickerson and Mike Dodds and Parkinson, {Matthew J.}",

year = "2013",

month = mar,

day = "16",

doi = "10.1007/978-3-642-37036-6_12",

language = "English",

isbn = "978-3-642-37035-9",

volume = "7792 LNCS",

series = "Lecture Notes in Computer Science",

publisher = "ACM",

pages = "189--208",

booktitle = "Programming Languages and Systems",

address = "United States",

note = "22nd European conference on Programming Languages and Systems (ESOP 2013) ; Conference date: 16-03-2013 Through 24-03-2013",

}

Wickerson, J, Dodds, M & Parkinson, MJ 2013, Ribbon proofs for separation logic. in Programming Languages and Systems: ESOP'13 Proceedings of the 22nd European conference on Programming Languages and Systems. vol. 7792 LNCS, Lecture Notes in Computer Science, vol. 7792, ACM, pp. 189-208, 22nd European conference on Programming Languages and Systems (ESOP 2013), Rome, Italy, 16/03/13. https://doi.org/10.1007/978-3-642-37036-6_12

Ribbon proofs for separation logic. / Wickerson, John; Dodds, Mike; Parkinson, Matthew J.
Programming Languages and Systems: ESOP'13 Proceedings of the 22nd European conference on Programming Languages and Systems. Vol. 7792 LNCS ACM, 2013. p. 189-208 (Lecture Notes in Computer Science; Vol. 7792).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Ribbon proofs for separation logic

AU - Wickerson, John

AU - Dodds, Mike

AU - Parkinson, Matthew J.

PY - 2013/3/16

Y1 - 2013/3/16

N2 - We present ribbon proofs, a diagrammatic system for proving program correctness based on separation logic. Ribbon proofs emphasise the structure of a proof, so are intelligible and pedagogical. Because they contain less redundancy than proof outlines, and allow each proof step to be checked locally, they may be more scalable. Where proof outlines are cumbersome to modify, ribbon proofs can be visually manoeuvred to yield proofs of variant programs. This paper introduces the ribbon proof system, proves its soundness and completeness, and outlines a prototype tool for validating the diagrams in Isabelle.

AB - We present ribbon proofs, a diagrammatic system for proving program correctness based on separation logic. Ribbon proofs emphasise the structure of a proof, so are intelligible and pedagogical. Because they contain less redundancy than proof outlines, and allow each proof step to be checked locally, they may be more scalable. Where proof outlines are cumbersome to modify, ribbon proofs can be visually manoeuvred to yield proofs of variant programs. This paper introduces the ribbon proof system, proves its soundness and completeness, and outlines a prototype tool for validating the diagrams in Isabelle.

U2 - 10.1007/978-3-642-37036-6_12

DO - 10.1007/978-3-642-37036-6_12

M3 - Conference contribution

SN - 978-3-642-37035-9

VL - 7792 LNCS

T3 - Lecture Notes in Computer Science

SP - 189

EP - 208

BT - Programming Languages and Systems

PB - ACM

T2 - 22nd European conference on Programming Languages and Systems (ESOP 2013)

Y2 - 16 March 2013 through 24 March 2013

ER -