Derivation of program properties from polymorphic types in modern functional and functionallogic languages
DFGGrants: Ableitung von Programmeigenschaften aus polymorphen Typen in modernen funktionalen und funktionallogischen SprachenAbstract:
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; socalled 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) functionallogic languages like Curry.Principal investigator:
Janis VoigtländerFunding:
Deutsche Forschungsgemeinschaft (DFG), Project Numbers: VO 1512/11 and VO 1512/12
The project was mainly supported with a research position for 45 person months.
The total funding volume for the first phase (VO 1512/11) was >156k Euro.
The total funding volume for the second phase (VO 1512/12) was >60k Euro (including >10k Euro overhead that went to the university).
Some papers on theoretical foundations:

S. Mehner, D. Seidel, L. Straßburger, and J. Voigtländer
Parametricity and Proving Free Theorems for FunctionalLogic Languages
at PPDP'14 
D. Seidel and J. Voigtländer
Refined Typing to Localize the Impact of Forced Strictness on Free Theorems
in Acta Informatica, 2011 
D. Seidel and J. Voigtländer
Improvements for Free
at QAPL'11 
J. Christiansen, D. Seidel, and J. Voigtländer
An Adequate, Denotational, FunctionalStyle Semantics for Typed FlatCurry without Letrec
Technical Report IAITR20111, University of Bonn, March 2011. 
D. Seidel and J. Voigtländer
Automatically Generating Counterexamples to Naive Free Theorems
at FLOPS'10 
J. Christiansen, D. Seidel, and J. Voigtländer
Free Theorems for Functional Logic Programs
at PLPV'10 
F. Stenger and J. Voigtländer
Parametricity for Haskell with Imprecise Error Semantics
at TLCA'09 
P. Johann and J. Voigtländer
A family of syntactic logical relations for the semantics of Haskelllike languages
in Information and Computation, 2009
Some papers on applications:

J. Christiansen and D. Seidel
Minimally Strict Polymorphic Functions
at PPDP'11 
D. Seidel and J. Voigtländer
Proving Properties About Functions on Lists Involving Element Tests
in WADT'10 revised selected papers, 2012 
J. Voigtländer
Free Theorems Involving Type Constructor Classes
at ICFP'09
A video of the conference presentation is available here.
Implementations:

We have a library and tool for generating free theorems from Haskell types.
See the announcement here, as well as reasonably uptodate information here.
The library and a shellbased application built on top of it can be downloaded in source form here and here.
A web interface (supporting PNG, PDF, and TEX output) to the tool is accessible here.  The implementation of the algorithm presented at FLOPS'10 is accessible via a web interface here.
 The implementation of the algorithm developed in the Acta Informatica paper is accessible via a web interface here.