Greg Morrisett
Harvard University
Abstract:
The Tofte-Talpin region calculus supports programmer-controlled memory
management. Objects are allocated within regions, and regions are
created and destroyed with a lexically-scoped "letregion" construct,
leading to last-in-first-out (LIFO) region lifetimes. A
sophisticated type-and-effect system is used to ensure that references
to a deallocated region cannot be dereferenced. The TT type
system forms the basis of next-generation systems languages such as
Cyclone, Cqual, and Vault.
In this talk, I will sketch a translation of the TT calculus to a much
simpler target language without effects. The target language is a
variant of the polymorphic, linear lambda calculus. The
translation is broken into two major steps: the first step
encodes effects using a combination of polymorphism and an indexed
family of store monads. The second step eliminates the monads by
leveraging linearity. A key advantage of the target language is
that regions need not be allocated in a lexically-
scoped, LIFO fashion, and regions become first-class objects.
This is ongoing work with Matthew Fluet and Amal Ahmed.
Host: Bob Harper
Appointments: Norene Mears
Principles
of Programming Seminars
Friday, April 1, 2005
3:30 p.m.
Wean Hall 8220