| 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.
|