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
Contributor : Lutz Straßburger Connect in order to contact the contributor
Submitted on : Thursday, December 18, 2014 - 11:54:11 AM
Last modification on : Thursday, January 20, 2022 - 5:30:46 PM
Long-term archiving on: : Saturday, April 15, 2017 - 4:31:15 AM


Files produced by the author(s)




Stefan Mehner, Daniel Seidel, Lutz Strassburger, 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⟩



Record views


Files downloads