[TYPES] HOAS and Denotational Semantics

[Klaus Ostermann]

Dear list members,

I wonder whether there is any work on denotational semantics based on a
higher-order abstract
syntax representation of the terms.

To maintain compositionality, it seems to me that a HOAS term of type
"Term -> Term" has
to be given a denotation of type "Value -> Value". There are some papers
that deal with the problem
of how to write "folds" on HOAS terms, such as the "Boxes go bananas"
paper by Washburn and Weirich,
but none of the works I have seen specifically addresses the problem of
defining a denotational semantics

Surprisingly, the original HOAS paper by Pfenning and Elliott touches on
the issue of denotational
semantics and claims that it "significantly simplifies denotational
semantics specifications", but that paper
does not say anything about the problem how to compute "Value -> Value"
from "Term -> Term".

Hence my question is whether there are any works that elaborate on this
issue. Any pointers
will be appreciated.

Thanks in advance,

  Klaus