Skip to content

Instantly share code, notes, and snippets.

Show Gist options
  • Save ComFreek/9b7f64a294bd2b7d0d952af6ff2402c2 to your computer and use it in GitHub Desktop.
Save ComFreek/9b7f64a294bd2b7d0d952af6ff2402c2 to your computer and use it in GitHub Desktop.
Explanation of Higher Order Abstract Syntax in Twelf and MMT

As a follow-up to today's discussion of HOAS, here is another example: https://en.wikipedia.org/wiki/Higher-order_abstract_syntax#Use_in_logical_frameworks

That example is based on Twelf, which for the purpose of that example, you can think of MMT. In fact, Twelf can be seen as a predecessor of MMT.

Apparently, there's also this classic paper by Pfenning and Elliott on HOAS. The paper's presentation might be a bit too far away from MMT for it to be easily understandable to you. But Section 2 ("motivating examples") might still be of interest to you: it mentions problems of substitution and variable occurrences, which you usually have if you're representing bound variables as mere "string references". I think you might be able to understand bits even if not all of the syntax. (Neither do I understand their syntax by mere glancing.)

By employing, HOAS we completely forego those problems by using meta-level functions (namely from LF). (Internally, these do work with "string references", though, cf. OMV in MMT source code.)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment