An Adequate, Denotational, Functional-Style Semantics for Typed FlatCurry
| Authors: | J. Christiansen, D. Seidel, and J. Voigtländer |
|---|---|
| Published: | In 19th International Workshop on Functional and (Constraint) Logic Programming (WFLP'10, acceptance rate 12/15), Madrid, Spain, Revised Selected Papers (acceptance rate 8/12), volume 6559 of LNCS, pages 119-136, Springer, 2011. |
| DOI: | 10.1007/978-3-642-20775-4_7 |
| BibTeX: | CSV11a.bib |
| Abstract: | With the aim of putting type-based reasoning for functional logic languages, as recently explored by Christiansen et al. (2010), on a formal basis, we develop a denotational semantics for a typed core language of Curry. Dealing with the core language FlatCurry rather than with full Curry suffices, since there exists a type-preserving translation from the latter into the former. In contrast to existing semantics for functional logic languages, we deliberately approach the problem "from the functional side". That is, rather than adapting approaches previously known from the study of (resolution-like) semantics for logic languages, we aim for a semantics in the spirit of standard denotational semantics for the polymorphic lambda calculus. We claim and set out to prove that the presented semantics is adequate with respect to an existing operational semantics. A particularly interesting aspect, we think, is that we give the first denotational treatment of recursive let-bindings in combination with call-time choice. |
| Rights: | Copyright held by Springer. |
We found that two of the conjectures in the paper do not hold, see the online appendix for details. There is also a revised version available as a technical report, incorporating the corrections, see here.