Parametricity and Proving Free Theorems for Functional-Logic Languages

Stefan Mehner 1 Daniel Seidel 1 Lutz Straßburger 2, 3 Janis Voigtländer 1
1 University of Bonn
2 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
3 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
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.
Type de document :
Communication dans un congrès
Principles and Practice of Declarative Programming, PPDP 2014, Sep 2014, Canterbury, United Kingdom. 〈10.1145/2643135.2643147〉
Liste complète des métadonnées

Littérature citée [16 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01092357
Contributeur : Lutz Straßburger <>
Soumis le : jeudi 18 décembre 2014 - 11:54:11
Dernière modification le : mercredi 14 novembre 2018 - 16:14:01
Document(s) archivé(s) le : samedi 15 avril 2017 - 04:31:15

Fichier

ppdp2014-final.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

X | INRIA | LIX | X-LIX | PARISTECH | X-DEP-INFO

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〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

695

Téléchargements de fichiers

204

Contact


archive-ouverte@inria.fr