Free Theorems for Functional Logic Programs

The paper is available via the ACM DL Author-ize feature:

ACM DL Author-ize service Free Theorems for Functional Logic Programs

Authors: J. Christiansen, D. Seidel, and J. Voigtländer
Published: In 4th Workshop on Programming Languages meets Program Verification (PLPV'10, acceptance rate 7/10), Madrid, Spain, Proceedings, pages 39-48, ACM, January 2010.
DOI: 10.1145/1707790.1707797
BibTeX: CSV10.bib
Abstract: Type-based reasoning is popular in functional programming. In particular, parametric polymorphism constrains functions in such a way that statements about their behavior can be derived without consulting function definitions. Is the same possible in a strongly, and polymorphically, typed functional logic language? This is the question we study in this paper. Logical features like nondeterminism and free variables cause interesting effects, which we examine based on examples and address by identifying appropriate conditions that guarantee standard free theorems or inequational versions thereof to hold. We see this case study as a stepping stone for a general theory, not provided here, involving the definition of a logical relation and other machinery required for parametricity arguments appropriate to functional logic languages.
Download: http://dl.acm.org/authorize?297480 (free)

An abstract-only version appeared in volume 44(11) of SIGPLAN Notices, page 7 (http://doi.acm.org/10.1145/1816027.1816035).