Project: Derivation of program properties from polymorphic types in modern functional languages

(German: Ableitung von Programmeigenschaften aus polymorphen Typen in modernen funktionalen Sprachen)

Abstract:

Both programmers and programming language developers need techniques to effectively and precisely reason about the behavior of programs. Typed functional programming languages are particularly amenable to such analysis. In particular, the theory of relational parametricity allows to derive statements about program behavior from (polymorphic) types alone; so-called free theorems. This theory, however, is underdeveloped for many aspects of modern functional languages. For example, important type constructs and other features of Haskell are not taken into account appropriately, which leads to considerable restrictions with respect to potential applications. The project aims to provide new theoretical foundations and refinements of relational parametricity while including such practically relevant features, as well as to apply the theoretical development (for example, to program transformations).

Principal investigator:

Janis Voigtländer

Funding:

Deutsche Forschungsgemeinschaft (DFG), Project Number: VO 1512/1-1

The project is mainly supported with a full research position for 36 months, currently held by Daniel Seidel (at 75%).

In terms of grant money, this is the current "completion status" of the project:

Produced Software:

Recent papers:

Last Updated: February 2010, Janis Voigtlaender.