BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:F^o: Lightweight Linear F - Steve Zdancewic
DTSTART:20091012T114500Z
DTEND:20091012T130000Z
UID:TALK20696@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:Ideas from Girard's linear logic have been applied to many pro
 gramming language problems\, ranging from alias analysis and memory manage
 ment to protocol enforcement and session types.  Despite these success sto
 ries\, we have yet to see support for linear types in a general-purpose fu
 nctional language.  We conjecture that this is because traditional formula
 tions of linear types can lead to awkward programming models or interact p
 oorly with other language features like polymorphism.\n\nIn this talk\, I 
 will present F^o^\, a variant of System F that uses kinds to distinguish b
 etween linear and unrestricted types. This design is intended to be simple
 \, familiar\, and expressive: F^o^ lets programmers enforce their own prot
 ocol abstractions through the power of linearity and polymorphism\, yet it
 s typing discipline is lightweight enough to expose in a surface language.
 \n\nI will illustrate F^o^'s utility through examples and compare its supp
 ort for linearity to alternative designs\, namely type qualifiers and the 
 ! modality.\n\nThis is joint work with Karl Mazurak\, Jianzhou Zhao\, and 
 Aileen Zheng at the University of Pennsylvania.\n
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR