BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent
  Reasoning - Kasper Svendsen
DTSTART:20141126T130000Z
DTEND:20141126T140000Z
UID:TALK53617@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:(joint work with Ralf Jung\, David Swasey\, Filip Sieczkowski\
 , Aaron Turon\, Lars Birkedal and Derek Dreyer)\n\nAbstract:\nWe present I
 ris\, a concurrent separation logic with a simple premise:\nmonoids and in
 variants are all you need. Partial commutative monoids\nenable us to expre
 ss—and invariants enable us to enforce— user-defined\nprotocols on sha
 red state\, which are at the conceptual core of most recent\nprogram logic
 s for concurrency. Furthermore\, through a novel extension of\nthe concept
  of a view shift\, Iris supports the encoding of logically atomic\nspecifi
 cations\, i.e.\, Hoare-style specs that permit the client of an operation\
 nto treat the operation essentially as if it were atomic\, even if it is n
 ot.\n
LOCATION:SS03
END:VEVENT
END:VCALENDAR