[TYPES] HOAS versus meta reasoning

[Andrew Gacek]

Hi Andrei,

There has been research on this topic for over a decade, begun by Dale
Miller and Ray McDowell (who picked up on earlier work by Peter
Schroeder-Heister and Girard), continued by Alwen Tiu and Dale Miller
and now including several others like David Baelde, Gopalan Nadathur
and myself. There is also a system called Abella
(http://abella.cs.umn.edu) that incorporates this style of reasoning.
Some of the highlights of this research are:

 * Reasoning with higher-order abstract syntax in a logical framework,
by Raymond McDowell and Dale Miller (ToCL 2002). In this paper
McDowell and Miller present a logic with HOAS, recursive definitions,
and natural number induction. Using this logic they are able to prove
various theorems such as subject reduction for the lambda calculus,
but in each theorem when they use the inductive hypothesis, they do so
on closed HOAS terms. The reason is that they have trouble encoding
the free variables in a logical way.

* A proof theory for generic judgments, by Dale Miller and Alwen Tiu
(LICS 2005), and A logical framework for reasoning about logical
specifications, by Alwen Tiu (PhD 2004). In the first paper Miller and
Tiu introduce a new logical quantifier called nabla which allows them
to overcome the previous issue with encoding free variables. In
particular, they are able to elegantly encode many notions from the
pi-calculus. The second work is Tiu's PhD thesis in which he adds a
notion of induction and coinduction on recursive definitions to the
logic.

* A logic for reasoning about generic judgments, by Alwen Tiu (LFMTP
2006) and Combining generic judgments with recursive definitions, by
Andrew Gacek, Dale Miller, and Gopalan Nadathur (LICS 2008). In the
first paper Tiu notices that the original formulation of nabla is
often too strict when reasoning inductively, and so he defines an
alternative treatment of nabla which acts more naturally. In the
latter paper, Miller, Nadathur, and I note that the typical treatment
of recursive definitions does not allow us to analyze the structure of
terms that are built up using nabla, thus we propose an extension to
recursive definitions to handle this.

* Reasoning in Abella about structural operational semantics
specifications, by Andrew Gacek, Dale Miller, and Gopalan Nadathur
(LFMTP 2008). I highlight this paper because it presents an extended
example (weak normalization for simply-typed lambda calculus) of how
reasoning is conducted using the logic developed in the LICS 2008
paper. For a practical perspective of reasoning, this may be the most
up-to-date and relevant work.

The Abella website has links to many of these papers and some
additional references. Also, if you are looking for practical
examples, the website has various applications that have been
developed using the logic from the LICS 2008 paper. This includes
things like POPLmark, Church-Rosser, normalization results on the
lambda-calculus, and cut-elimination for a sequent calculus.

If you are more interested in how exactly we allow HOAS to interact
with induction, I can sketch that here. The idea is that we allow
induction on recursive definitions, and not specifically on HOAS
terms. Thus, for example, if one is reasoning about evaluation of an
expression E to a value V, we will induct on the predicate (eval E V).
Thus we can do induction on the structure of a HOAS term by writing
down a predicate which recognizes the terms of interest and then
inducting on that predicate. This is the essential idea, though things
are more complicated in detail.

Finally, there is a lot of work in this area based on LF and Twelf
that I have not mentioned, but hopefully somebody who is more involved
in that work can describe it here.

-Andrew Gacek



On Wed, Nov 12, 2008 at 1:26 PM, Andrei Popescu <uuomul at yahoo.com> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Dear Type Theorists and Practioners,
>
> 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.)
>
> Thank you in advance,
>   Andrei Popescu
>
>
>
>
>
>