| |
|
| |
|
Amal Ahmed
Harvard University
Taming Mutable State
April 19, 2006 10:00am
Abstract:
One area where conventional type systems provide limited help is in the specification and enforcement of memory management and aliasing invariants. I'll introduce a relatively simple framework, based on substructural logic, that provides the core mechanisms necessary to restrict the number of times and the order in which data is used. We have shown that such substructural type systems can support deallocation of memory, strong (type-varying) updates, storage of unique (unaliased) objects in shared (aliased) references, as well as 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 are useful for verifying the correctness of program transformations such as compiler optimizations. Logical relations for simple type systems are straightforward, but scaling the method up to handle memory updates (as in Java or ML) demands the use of nontrivial mathematical theories such as domain theory and category theory. The key problem is that logical relatons, 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.
If you have questions, or would like to meet the speaker, please contact Ponda at 4-1994 or pondabarnes@tti-c.org. For information on future TTI-C talks or events, please go to the TTI-C Events page.