[TYPES] HOAS versus meta reasoning

[Brian Huffman]

Quoting Dan Licata <drl at cs.cmu.edu>:

> There has also been a good deal of work on representing variable binding
> using a computational function space (e.g., in Coq), but I will defer
> to others to provide the best citations.
>
> -Dan
>
>

I would also be interested in citations about variable binding using  
computational function space, if anyone knows any good ones.

In particular, I am thinking about using domain theory  
(Isabelle/HOLCF) and the continuous function space for doing HOAS. I  
would appreciate any pointers to relevant work.

- Brian