Computer Science Colloquium

Taming Mutable State

Amal Ahmed
Harvard University

Friday, April 14, 2006 11:30 A.M.
Room 1302 Warren Weaver Hall
251 Mercer Street
New York, NY 10012-1185

Colloquium Information:


Clark, (212) 998-3105


One area where conventional type systems provide limited help is in the specification and enforcement of memory usage invariants. For instance, one cannot usually express the invariant that deallocated memory must never be accessed in the future. I'll introduce a relatively simple framework, based on linear logic, that provides the core mechanisms necessary to restrict the number and order of uses of data and operations. We have shown that such substructural type systems can support strong (type-varying) updates, deallocation of memory, storage of unique (unaliased) objects in shared (aliased) references, temporarily treating shared references as unique, and region-based memory management.

I will also discuss a powerful proof technique known as logical relations, useful for establishing many important properties of typed languages including termination, safety, and parametricity. In particular, logical relations yield a sound principle for proving program equivalence and for verifying the correctness of program transformations such as compiler optimizations. Logical relations for simple type systems are straightforward, but to scale the method up to handle memory updates (as in Java or ML) requires a strong grasp of category theory. The key problem is that logical relations, normally defined by induction on types, are no longer well founded in the presence of mutable state. I'll describe logical relations that permit simple and direct proofs based on operational reasoning, without the need for complicated mathematics.

top | contact