Jan Christiansen, Daniel Seidel, Janis Voigtländer. An Adequate, Denotational, Functional-Style Semantics for Typed FlatCurry. In Julio Mariño, editor, Functional and Constraint Logic Programming - 19th International Workshop, WFLP 2010, Madrid, Spain, January 17, 2010. Revised Selected Papers. Volume 6559 of Lecture Notes in Computer Science, pages 119-136, Springer, 2010. [doi]
With the aim of putting type-based reasoning for functional logic languages, as recently explored by Christiansen et al. (PLPV 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.