An Adequate, Denotational, Functional-Style Semantics for Typed FlatCurry without Letrec

Authors: J. Christiansen, D. Seidel, and J. Voigtländer
Published: Technical Report IAI-TR-2011-1, University of Bonn, March 2011.
BibTeX: CSV11b.bib
Abstract: With the aim of putting type-based reasoning for functional logic languages, as recently explored by Christiansen et al. (PLPV'10), 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. Due to problems with recursive let-bindings in combination with call-time choice (discussed in an appendix), we give the denotational semantics in the presence of non-recursive let-expressions only.
Download: AnAdequateDenotationalFunctionalStyleSemanticsForTypedFlatCurryWithoutLetrec.pdf