BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Ribbon Proofs for Separation Logic - John Wickerson
DTSTART:20120620T123000Z
DTEND:20120620T124500Z
UID:TALK38677@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:(This is a 15-minute practice talk for next week's LICS confer
 ence. 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 separatio
 n logic. By emphasising the structure of a proof\, ribbon proofs are intel
 ligible and hence useful pedagogically. Because they are free from the red
 undancy endemic in proof outlines\, and allow each proof step to be checke
 d locally\, they are highly scalable. Where proof outlines are cumbersome 
 to modify\, ribbon proofs (with variables-as-resource enabled) can be visu
 ally manoeuvred\, perhaps to accommodate various program transformations. 
 This paper introduces the ribbon proof system\, proves its soundness and c
 ompleteness\, and outlines a prototype tool for validating the diagrams in
  Isabelle.
LOCATION:FW26
END:VEVENT
END:VCALENDAR