BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Tunable Static Inference for Generic Universe Types - Werner M Die
 tl\, University of Washington
DTSTART:20110802T100000Z
DTEND:20110802T110000Z
UID:TALK32208@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Object ownership is useful for many applications\, including p
 rogram verification\, thread synchronization\, and memory management. Howe
 ver\, the annotation overhead of ownership type systems hampers their wide
 spread application. This talk addresses this issue by presenting a tunable
  static type inference for Generic Universe Types. In contrast to classica
 l type systems\, ownership types have no single most general typing. Our i
 nference chooses among the legal typings via heuristics. Our inference is 
 tunable: users can indicate a preference for certain typings by adjusting 
 the heuristics or by supplying partial annotations for the program. We pre
 sent how the constraints of Generic Universe Types can be encoded as a boo
 lean satisfiability (SAT) problem and how a weighted Max-SAT solver finds 
 a correct Universe typing that optimizes the weights. We implemented the s
 tatic inference tool\, applied our inference tool to four real-world appli
 cations\, and inferred interesting ownership structures.
LOCATION:Small lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR