Web appendix of the paper

Hybrid:

a Definitional Two Level Approach to Reasoning

with Higher Order Abstract Syntax.

Amy Felty and Alberto Momigliano.

Hybrid:

a Definitional Two Level Approach to Reasoning

with Higher Order Abstract Syntax.

Amy Felty and Alberto Momigliano.

The Hybrid package has been developed for Coq and Isabelle/HOL

- A tar file for the Coq
version version 8.0pl3 is here.
This follows very closely the paper except chapter 5 which it is not
encoded.

As far as Isabelle/HOL is concerned,
the situation is more complicated due to the fact new versions of HOL
are not conservative w.r.t. the previous ones and porting theories
through versions may be painful. For example the jump from HOL 2005 to
2007 more or less eliminated the tactical language and the
interaction with the shell. So the the Isabelle/HOL code will be
organized around
versions. If the reader feel the need for other files for better
understanding we will be happy to post them.

- Isabelle/HOL 2002 (and 2003). Here
we present only the original Hybrid infrastructure without any 2-level
reasoning, although both case studies of the paper have been
fully verified. Note that the tar contains the file BiAbstr.thy to
which we refer in the paper at page 12.

- Isabelle/HOL 2005. Here I (i.e., AM) have to come clean. The two case studies are actually based on what we have called Hybrid. Therefore SL universal quantification does not require the "proper" annotation, since the latter is a type. Further I have removed the "isterm" annotations that would have made the Olli example more difficult to follow. Similarly for the other example for which, however, we have the comfort of the Coq version doing the right thing. So here's what we do:

- Isabelle/HOL 2007. We re-present Hybrid.thy
by Alan Martin which implements Hybrid
0.2. For completeness we also add the porting of Expr.thy
and Abstr.thy from Isabelle/HOL 2005 to
ISAR,
noting that they lack all the new features that Hybrid
0.2 offers

- Isabelle/HOL 2008. Here's the
porting Hybrid 0.2 to Isabelle 2008, as well as Expr.thy
and Abstr.thy, again by Alan
Martin.