Friday, 2 March 2007, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B126
Slides from the talk [pdf]
Abstract: Contracts specify pre- and postconditions on program functionality. At the same time, they allow to assign blame to a part of the program whenever a contract is violated.
While contracts have been around for quite some time, they only recently have been explored in the context of functional languages with (possibly polymorphic) higher-order functions and algebraic data types.
Contracts are similar to types, but are usually checked at run-time. For example, a contract that specifies the strings of length 3 might be written as follows:
{ x : String | length x == 3 }
The compiler would check statically that the value in question is a string, and generate a run-time check to verify the condition on its length. In this talk, we present a type system for an ML-like language that pursues this idea. We illustrate the use of contracts in this language with several examples. (Joint work with Ralf Hinze and Andreas Schmitz.)