Twelf and HOAS

[Joseph Abrahamson]

There was a question posted on the Hackpad from meeting 1 asking about HOAS and Twelf. Does anyone in the group with experience with Twelf want to talk about how HOAS and abts relate?

> What is higher-order abstract syntax, e.g. as seen in the Twelf programming language? (:+1:)(:+1:)(:+1:)

[Jonathan Sterling]

LF and ABTs are analogous in the sense that they are both logical frameworks / metalanguages which are used to account for the binding and scope of object languages (this is the HOAS methodology). LF is just a much more elaborate system than the ABT framework (LF is a higher-order type theory, whereas ABTs are a lot more like algebraic theories).

[Danny Gratzer]

Building on what Jon said, the 10k foot overview is that in LF we start with a dependently-typed lambda calculus

with basically just dependent functions. We then define new constants to represent the constructs of the

object language we're trying to describe.

We use the function space of the typed lambda calculus to represent binding, then we get 

substitution as just function application and alpha equivalence is handled by the fact that LF's

functions alpha vary as well. This means that most of the woes with representing binding just

go away because we use the underlying frameworks notion of binding.

twelf.org also contains some good explanations of how this works. 

[Mark Farrell]

Cool, thanks; was wondering about this.

[Steven Shaw]

Huh, never would have thought of ABTs as a logical framework. Something to ponder on.

--
You received this message because you are subscribed to the Google Groups "Type Theory Study Group" group.
To unsubscribe from this group and stop receiving emails from it, send an email to type-theory-study...@googlegroups.com.
To post to this group, send email to type-theory...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/type-theory-study-group/5626b468-18b5-480c-ad13-a8823f01a3e9%40googlegroups.com.

For more options, visit https://groups.google.com/d/optout.