BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Separation Logic and Graphical Models - John Wickerson (University
  of Cambridge)
DTSTART:20101025T114500Z
DTEND:20101025T130000Z
UID:TALK27333@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:We describe work in progress to develop a new model of Separat
 ion Logic that is based not on heaps\, but on execution traces. The star-o
 perator now composes not sets of heaps (i.e. assertions)\, but sets of tra
 ces -- that is\, programs. We then use the star-operator to define a compo
 sitional denotational semantics for a concurrent programming language. Hap
 pily\, we can use the laws of Separation Logic to reason algebraically abo
 ut our semantics.\n\nThis talk is based on joint work with Tony Hoare.\n
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR