Ribbon Proofs for Separation Logic

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

• John Wickerson
• Wednesday 20 June 2012, 13:30-13:45
• FW26.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.