BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Semantics Lunch (Computer Laboratory)
SUMMARY:Ribbon Proofs for Separation Logic - John Wickerso
n
DTSTART;TZID=Europe/London:20120620T133000
DTEND;TZID=Europe/London:20120620T134500
UID:TALK38677AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/38677
DESCRIPTION:(This is a 15-minute practice talk for next week's
LICS conference. Joint work with Mike Dodds and M
atthew Parkinson.) Building on work by Bean\, we p
resent the ribbon proof as a diagrammatic alternat
ive to the proof outline for constructing and pres
enting program proofs in separation logic. By emph
asising the structure of a proof\, ribbon proofs a
re intelligible and hence useful pedagogically. Be
cause 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 p
roofs (with variables-as-resource enabled) can be
visually manoeuvred\, perhaps to accommodate vario
us 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.
LOCATION:FW26
CONTACT:Peter Sewell
END:VEVENT
END:VCALENDAR