[TYPES] HOAS versus meta reasoning

[Dan Licata]

On Nov12, Andrei Popescu wrote:
> I would like to know what is the state of the art in taming the
> interaction between HOAS (higher order abstract syntax) and
> meta-reasoning/inductive reasoning/recursive definitions.  (I am aware
> of some of the work, but very probably I am not aware of the latest
> progress.)

Hi Andrei, 

Funny you should ask!  You can get a hands-on feel for how this issue is
addressed in Twelf by coming to the Twelf Tutorial on January 19,
co-located with this year's POPL:

  http://twelftutorial.plparty.org/

Registration is now open!


If you can't make the tutorial, there are tons of examples of induction
on HOAS on the Twelf Wiki:
  http://twelf.plparty.org/

You should also look at two newer functional languages for computing
with LF terms, Delphin:
  http://cs-www.cs.yale.edu/homes/delphin/
and Beluga:
  http://www.cs.mcgill.ca/~complogic/beluga/

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.


An alternative approach, which I have been investigating with Noam
Zeilberger and Bob Harper, is to integrate an LF-like function space for
representing binding, along with a standard computational function
space, as two different types in a single type theory.  See our LICS'08
paper "Focusing on Binding and Computation", which is linked from here:

  http://www.cs.cmu.edu/~drl/pubs.html


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