[TYPES] HOAS and Denotational Semantics

[Adam Chlipala]

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

I wrote a paper on applying the "Boxes Go Bananas" style of HOAS in Coq 
to give (non-Turing-complete) languages denotational semantics and 
verify program transformations:
    http://adam.chlipala.net/papers/PhoasICFP08/