Parametricity and Proving Free Theorems for Functional-Logic Languages

The paper is available via the ACM DL Author-ize feature:

ACM DL Author-ize service Parametricity and Proving Free Theorems for Functional-Logic Languages

Authors: S. Mehner, D. Seidel, L. Straßburger, and J. Voigtländer
Published: In 16th International Symposium on Principles and Practice of Declarative Programming (PPDP'14, acceptance rate 22/43), Canterbury, UK, Proceedings, pages 19-30, ACM, September 2014.
DOI: 10.1145/2643135.2643147
BibTeX: MSSV14.bib
Abstract: The goal of this paper is to provide the required foundations for establishing free theorems - statements about program equivalence, guaranteed by polymorphic types - for the functional-logic programming language Curry. For the sake of presentation we restrict ourselves to a language fragment that we call CuMin, and that has the characteristic features of Curry (both functional and logic). We present a new denotational semantics based on partially ordered sets without limits. We then introduce an intermediate language called SaLT that is essentially a lambda-calculus extended with an abstract set type, and again give a denotational semantics. We show that the standard (logical relations) techniques can be applied to obtain a general parametricity theorem for SaLT and derive free theorems from it. Via a translation from CuMin to SaLT that fits the respective semantics, we then derive free theorems for CuMin.
Download: (free)