BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Theory of Type-directed Coercion Insertion - Mike Hicks (Univers
 ity of Cambridge)
DTSTART:20090317T130000Z
DTEND:20090317T140000Z
UID:TALK16358@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:A number of important program rewriting scenarios can be recas
 t as type-directed coercion insertion. These range from more theoretical a
 pplications such as coercive subtyping\, and supporting overloading in typ
 e theories\, to more practical applications such as integrating static and
  dynamically typed code using gradual typing\, and inlining code to enforc
 e security policies such as access control and provenance tracking. In thi
 s paper we give a general theory of type-directed rewriting based on gener
 ating and inserting coercions. We specifically explore the inherent tradeo
 ff between expressiveness\nand ambiguity---the more powerful the strategy 
 for generating coercions\, the greater the possibility of several\, semant
 ically-distinct rewritings for a given program. We consider increasingly p
 owerful coercion generation strategies\, work out example applications sup
 ported by the increased power (including those mentioned above)\, and iden
 tify the inherent ambiguity problems of each setting\, along with various 
 techniques to tame the ambiguities.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR
