University of Cambridge > > Semantics Lunch (Computer Laboratory) > F^o: Lightweight Linear F

F^o: Lightweight Linear F

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

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 Fo, 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: Fo 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 Fo’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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity