[Pl-seminar] Semantics Seminar Schedule

[Mitchell Wand]

NU Programming Languages Seminar
Wednesday, 11/30/05
11:45-1:30 pm
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Type-systems for Region-based Memory Management

Matthew Fluet
Harvard University

Region-based memory management offers a healthy compromise in tuning a
program's memory usage; by reclaiming groups of related objects
wholesale, region-based languages may avoid both the inefficiency of
garbage collectors and the tedium of malloc/free.  Type systems for
region-based languages further enhance their utility by statically
catching (possibly) erroneous use of the region primitives.  In this
talk, we'll look at three "flavors" of type systems for region-based
languages:
   * a type-and-effect system (a la Tofte-Talpin)
   * a monadic type system
   * a sub-structural type system
Our goal is to demonstrate that we may successively encode the
type-and-effect system into the monadic type system and monadic type
system into the sub-structural type system.

The essence of the first encoding is to translate effects to an
indexed monad, inspired by (and generalizing) the ST monad of
Launchbury and Peyton Jones.  The upshot of this translation is that
we are able to trade the subtleties of an effect system for the
simplicity of a monadic system, where plain old parametric
polymorphism (a la System F) provides sufficient encapsulation.

However, both the type-and-effect system and the monadic type system
rquire that regions have last-in-first-out (LIFO) lifetimes following
the block structure of the language.  This places sever restrictions
on when objects may be effectively reclaimed and many natural programs
may give rise to (unbounded) leaks when compard to a garbage collected
implementation.  Hence, we introduce a sub-structural type system that
eliminates the LIFO restriction.  The key idea is to separate the
lifetime of a region from the scope of the region's name, by providing
explicit region creation and destruction primitives.

The essence of the second encoding, then, is to "break open" the monad
and reveal it's store passing implementation.  Furthermore, the
sub-structural type system allows us to faithfully encode even more
advanced features, such as Cyclone's dynamic regions and unique
pointers.

Upcoming Events:

stay tuned...

--Mitch