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

DFG-Grants: Ableitung von Programmeigenschaften aus polymorphen Typen in modernen funktionalen und 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 was mainly supported with a research position for 45 person months.

The total funding volume for the first phase (VO 1512/1-1) was >156k Euro.

The total funding volume for the second phase (VO 1512/1-2) was >60k Euro (including >10k Euro overhead that went to the university).

Some papers on theoretical foundations:

Some papers on applications:

Implementations:

An unexpected application of the approach presented in the ICFP'09 paper: