University of Cambridge > > Semantics Lunch (Computer Laboratory) > Ribbon Proofs for Separation Logic

Ribbon Proofs for Separation Logic

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Peter Sewell.

(This is a 15-minute practice talk for next week’s LICS conference. Joint work with Mike Dodds and Matthew Parkinson.) Building on work by Bean, we present the ribbon proof as a diagrammatic alternative to the proof outline for constructing and presenting program proofs in separation logic. By emphasising the structure of a proof, ribbon proofs are intelligible and hence useful pedagogically. Because they are free from the redundancy endemic in proof outlines, and allow each proof step to be checked locally, they are highly scalable. Where proof outlines are cumbersome to modify, ribbon proofs (with variables-as-resource enabled) can be visually manoeuvred, perhaps to accommodate various program transformations. This paper introduces the ribbon proof system, proves its soundness and completeness, and outlines a prototype tool for validating the diagrams in Isabelle.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity