Contracts and types

Andres Löh

Universität Bonn

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.)

Tarmo Uustalu
Last update 12.3.2007