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

VO 1512/1-1: Ableitung von Programmeigenschaften aus polymorphen Typen in modernen funktionalen Sprachen
VO 1512/1-2: Ableitung von Programmeigenschaften aus polymorphen Typen in funktional-logischen 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). In particular, beside qualitative properties also quantitative properties (about program efficiency) should be derivable. Beside functional languages, we also target (in the second project phase) functional-logic languages like Curry.

Principal investigator:

Janis Voigtländer

Funding:

Deutsche Forschungsgemeinschaft (DFG), Project Numbers: VO 1512/1-1 and VO 1512/1-2

The project is mainly supported with a research position for 45 person months (applied for, and granted, personal resources for the first phase were 36 months at 100%, and for the second phase are 12 months, post-doc level, at 75%).

The total funding volume for the first phase (VO 1512/1-1) was 156.201,28 Euro.

The projected funding volume for the second phase (VO 1512/1-2) is 60.700 Euro (including 10.100 Euro overhead that go to the university).

Produced Software:

Recent papers:

Last Updated: September 2011, Janis Voigtlaender.