BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Mezzo - Jonathan Protzenko (from INRIA)
DTSTART:20130430T130000Z
DTEND:20130430T140000Z
UID:TALK45093@talks.cam.ac.uk
CONTACT:Raoul-Gabriel Urma
DESCRIPTION:Mezzo is a programming language in the tradition of ML\, where
  the usual\nconcept of a type is replaced by a more precise notion of a\n/
 permission/. Permissions allow one to describe in an accurate manner\nhow 
 objects are laid out in memory -- more specifically\, permissions\ndescrib
 e the shape of the heap. Permissions also enable the programmer\nto contro
 l ownership of objects\, which turns out to be paramount in a\nconcurrent 
 setting.\n\nPermissions allow one to state more powerful invariants about 
 a\nprogram\, while still remaining within the bounds of a type system\;\nt
 herefore\, programs that previously could not be type-checked in ML can\nb
 e written in Mezzo. I will demonstrate the usage of patterns such as\nprog
 ressive initialization and strong update. I will also showcase a\nwork-in-
 progress prototype type-checker\, and give hints about future\nchallenges\
 , such as inference\, good primitives for concurrency\, and a\nproof of so
 undness.
LOCATION:FW11
END:VEVENT
END:VCALENDAR