[TYPES] HOAS versus meta reasoning

[Jonathan Aldrich]

> These LF-based approaches distinguish a representation layer (the LF
> logical framework) from a separate meta-language (Twelf/Delphin/Beluga).
> Inside LF, the types that you use to represent syntax are just base
> types, not inductive types, so there is no problem with constants like
> (lam : (exp -> exp) -> exp).  Externally to LF, the canonical forms of
> LF are treated as an inductive definition in a meta-language (such as
> Twelf/Delphin/Beluga), which allows you to compute and reason by
> structural induction on syntax.

One more LF-based approach is the education-focused SASyLF tool, which 
uses essentially the same meta-theory as Twelf, but is restricted to the 
Second-order Abstract Syntax (SASy) case.  The benefit of this 
restriction is that we can provide a surface syntax for the 
representation language and meta-language that is almost identical to 
the notation one might use in a paper proof, thus greatly decreasing the 
learning curve for students.  As in Twelf, binding in the represented 
language can be represented as binding in the representation language, 
and induction proceeds over canonical LF forms--but in the surface 
syntax, it just looks like induction over syntax and/or derivations.

SASyLF is currently being used in a couple of graduate type theory 
courses; for the tool, examples, and more information see:

http://www.sasylf.org/

Jonathan