[Colloquium] Reminder: Guest Speaker @ TTI-C Today (4/19/06)

[Katherine Cumming]

**********TTI-C Guest Speaker Today***********
                                 April 19, 2006
        Presented by:  Toyota Technological Institute at Chicago
 
 
Speaker:  Amal Ahmed, Harvard University  
Speaker's home page:  http://www.eecs.harvard.edu/~amal/
 
Date: Wednesday, April 19, 2006 
Location: TTI-C Conference Room 
Time:  10:00 am
 
Title:   Taming Mutable State
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
Katherine at 773-834-1994 or  <mailto:kcumming at tti-c.org> kcumming at tti-c.org

For information on future TTI-C talks and events, please go to the TTI-C
Events page:  http://www.tti-c.org/events.html.  TTI-C (1427 East 60th
Street, Chicago, IL  60637)
 
 
 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20060419/eb3bd23e/attachment.htm