Parametricity and Proving Free Theorems for Functional-Logic Languages
The paper is available via the ACM DL Author-ize feature:
| 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: | http://dl.acm.org/authorize?N05694 (free) |