F^o: Lightweight Linear F

Add to your list(s) Download to your calendar using vCal

• Steve Zdancewic
• Monday 12 October 2009, 12:45-14:00
• Room FW26, Computer Laboratory, William Gates Building.

If you have a question about this talk, please contact Sam Staton.

Ideas from Girard’s linear logic have been applied to many programming language problems, ranging from alias analysis and memory management to protocol enforcement and session types. Despite these success stories, we have yet to see support for linear types in a general-purpose functional language. We conjecture that this is because traditional formulations of linear types can lead to awkward programming models or interact poorly with other language features like polymorphism.

In this talk, I will present F^o, a variant of System F that uses kinds to distinguish between linear and unrestricted types. This design is intended to be simple, familiar, and expressive: F^o lets programmers enforce their own protocol abstractions through the power of linearity and polymorphism, yet its typing discipline is lightweight enough to expose in a surface language.

I will illustrate F^o’s utility through examples and compare its support for linearity to alternative designs, namely type qualifiers and the ! modality.

This is joint work with Karl Mazurak, Jianzhou Zhao, and Aileen Zheng at the University of Pennsylvania.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Computer Laboratory talks
• Room FW26, Computer Laboratory, William Gates Building
• School of Technology
• Semantics Lunch (Computer Laboratory)
• de239's list

Note that ex-directory lists are not shown.