BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Concurrent Logical Relation - Jacob Thamsborg (ITU)
DTSTART:20120530T133000Z
DTEND:20120530T143000Z
UID:TALK38347@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:I'll present recent work on a logical relation for\nshowing th
 e correctness of program transformations based on a new\ntype-and-effect s
 ystem for a concurrent extension of an ML-like language.\n\nWe'll see how 
 to use the model to verify interesting\nprogram transformations that rely 
 on effect annotations. In\nparticular\, I'll explain a Parallelization The
 orem\, which expresses\nwhen it is sound to run two expressions in paralle
 l instead of\nsequentially. The conditions are expressed solely in terms o
 f the\ntypes and effects of the expressions. To the best of our knowledge\
 ,\nthis is the first such result for a concurrent higher-order language\nw
 ith higher-order store and dynamic memory allocation.
LOCATION:FW26
END:VEVENT
END:VCALENDAR