Skip to Main content Skip to Navigation
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download

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

File

ppdp2014-final.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Stefan Mehner, Daniel Seidel, Lutz Straßburger, Janis Voigtländer. Parametricity and Proving Free Theorems for Functional-Logic Languages. Principles and Practice of Declarative Programming, PPDP 2014, Sep 2014, Canterbury, United Kingdom. ⟨10.1145/2643135.2643147⟩. ⟨hal-01092357⟩

Share

Metrics

Record views

946

Files downloads

637