Abstract: This talk presents 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 potentially useful for teaching. 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 is joint work with Mike Dodds and Matthew Parkinson, and is due to be presented at ESOP 2013.