TY - GEN
T1 - Parametricity and proving free theorems for functional-logic languages
AU - Mehner, Stefan
AU - Seidel, Daniel
AU - Straßburger, Lutz
AU - Voigtländer, Janis
PY - 2014/9/8
Y1 - 2014/9/8
N2 - 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.
AB - 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.
U2 - 10.1145/2643135.2643147
DO - 10.1145/2643135.2643147
M3 - Conference contribution
AN - SCOPUS:84968718649
T3 - PPDP 2014 - Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming
SP - 19
EP - 30
BT - PPDP 2014 - Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming
PB - Association for Computing Machinery, Inc
T2 - 16th International Symposium on Principles and Practice of Declarative Programming, PPDP 2014
Y2 - 8 September 2014 through 10 September 2014
ER -