Re: HOAS and Denotational Semantics

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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/