Abstract

(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.