Home

Have your AHOS and eat HOAS too!

Noam (uid 3913) announced on his weblog at the beginning of the year a technique that allows one to bridge the gap between meta-theoretic notions of function space and theory-internal notions, in a way that is compatible with structural induction over Higher-Order Abstract Syntax, by applying Reynolds' Definitional Interpreters for Higher-Order Programming Languages [pdf] (cf. LtU classic), and realised it as an implementation in Twelf.

That's a lot of ideas in one sentence, but since HOAS is in the air this month, I guess there are a good number of LtUers who will want to get to grips with this stuff.

Refs:

By Charles Stewart at 2009-10-22 10:27 | Type Theory | other blogs | 6974 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Thanks for the publicity.

Thanks for the publicity. Though, I worry the paper is a bit too specialized for getting across this simple idea (which like all good ideas goes back to John Reynolds). I wrote a smaller twelf example illustrating the basic technique on the language of arithmetic expressions (with binary operations imported from the meta-level) from our LICS08 paper with Dan Licata and Bob Harper. This example is also encoded in the paper by Atkey, Lindley, and Yallop mentioned on the other HOAS thread, so it serves as a point of reference. Actually I think the two techniques are pretty similar, though they look kind of dual: in one approach, you start with a higher-order meta level (Haskell) and use parametricity to recover higher-order abstract syntax, and in the other, you start with higher-order abstract syntax (LF) and a first-order meta level (Twelf), and use defunctionalization to recover a higher-order meta level.

By Noam at Fri, 2009-10-23 16:33 | login or register to post comments