BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Modular reasoning for modular concurrency - Aaron Turon\, Max Plan
 ck Institute for Software Systems
DTSTART:20130416T140000Z
DTEND:20130416T150000Z
UID:TALK44595@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Modular programming and modular verification go hand in hand\,
  but most existing logics for concurrency ignore two crucial forms of modu
 larity: *higher-order\nfunctions*\, which are essential for building reusa
 ble components\, and *granularity abstraction*\, a key technique for hidin
 g the intricacies of fine-grained concurrent data structures from their cl
 ients. This talk will present CaReSL\, the first logic to apply granularit
 y abstraction for modular verification of higher-order concurrent programs
 .  The talk is organized around a few simple but subtle examples that moti
 vate CaReSL's key ideas\, and that ultimately come together in a significa
 nt case study: the first formal proof of correctness for Hendler et al.'s 
 "flat combining" algorithm.\n
LOCATION:Small Lecture Theatre\, Microsoft Research Ltd\, 21 Station Road\
 , Cambridge\, CB1 2FB
END:VEVENT
END:VCALENDAR