| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Parametricity and Proving Free Theorems for Functional-Logic Languages
Abstract : The goal of this paper is to provide the required foundations forestablishing free theorems – statements about program equivalence,guaranteed by polymorphic types – for the functional-logic pro-gramming language Curry. For the sake of presentation we restrictourselves to a language fragment that we call CuMin, and that hasthe characteristic features of Curry (both functional and logic). Wepresent a new denotational semantics based on partially ordered setswithout limits. We then introduce an intermediate language calledSaLT that is essentially a lambda-calculus extended with an abstractset type, and again give a denotational semantics. We show that thestandard (logical relations) techniques can be applied to obtain ageneral parametricity theorem for SaLT and derive free theoremsfrom it. Via a translation from CuMin to SaLT that fits the respectivesemantics, we then derive free theorems for CuMin.
Cited literature [16 references]
https://hal.inria.fr/hal-01092357
Contributor : Lutz Straßburger <>
Submitted on : Thursday, December 18, 2014 - 11:54:11 AM
Last modification on : Thursday, January 7, 2021 - 3:40:14 PM
Long-term archiving on: : Saturday, April 15, 2017 - 4:31:15 AM
Contributor : Lutz Straßburger <>
Submitted on : Thursday, December 18, 2014 - 11:54:11 AM
Last modification on : Thursday, January 7, 2021 - 3:40:14 PM
Long-term archiving on: : Saturday, April 15, 2017 - 4:31:15 AM
File
ppdp2014-final.pdf
Files produced by the author(s)