[Colloquium] Matthias Blume talk - Thurs. 11/13 at TTI-C

[Meridel Trimble]

TOYOTA TECHNOLOGICAL INSTITUTE TALK

Speaker: Matthias Blume
TTI-C

Speaker’s homepage: http://www.tti-c.org/blume.shtml

Time: 12:15pm
Date:  Thursday, November 13th, 2003 
Place:  TTI-C (1427 East 60th Street, Second Floor - Press Building)
*FREE LUNCH PROVIDED*

Title: Sound Contract Exceptions

Abstract: Even in statically typed languages it is useful to have certain 
invariants checked dynamically.  Findler and Felleisen have  introduced a 
method of dynamically checking expressive higher-order types called 
contracts.  However, they give no soundness proof for this dynamic checking.  
We show that under a naive semantics for their contract expressions their 
algorithm is actually unsound and then give two ways of repairing this 
problem.  The soundness proofs for both of these repairs can be extended to 
general recursive types. 
 
In the first part of the talk I will give my own spin on Findler and 
Felleisen's algorithm, introduce the notion of types as sets of values, and 
show a counterexample (due to McAllester) to the correctness of the algorithm 
under a naive interpretation of types.  I will then show two different ways of 
fixing this problem: one by given a somewhat less naive interpretation of 
types, the other by using a different language of contract types. 

This is joint work with David McAllester.

If you have questions, or would like to meet the speaker, please contact 
Meridel at: 4-9873 or mtrimble 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.shtml