BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Diagrammatic Reasoning in Separation Logic - Matt Ridsdale (Univer
 sity of Cambridge)
DTSTART:20080917T120000Z
DTEND:20080917T130000Z
UID:TALK13418@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Diagrammatic reasoning seeks to put the use of diagrams on a p
 ar with the use of logic\, in terms of formality and automation. Humans of
 ten use diagrams informally to reason about specific instances of a genera
 l problem\, in order to work out a proof that applies to all cases.  This 
 can be modelled using the notion of a "schematic proof". I show how this a
 pplies to proving the specification of simple programs\, using execution t
 races to automatically suggest a complete program proof.\n\nThis will be a
  short talk\, probably around 15 minutes\, with hopefully plenty of questi
 ons and discussion afterwards. I'm showing a poster at a conference the fo
 llowing weekend\, so it will essentially be a slightly extended poster pre
 sentation in order to get some feedback.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR
