Greg Morrisett
Harvard University


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