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:
- First, install the Hybrid0.2 architecture as described by
the INSTALL file in this tar.
- Here are the files for a 2-level proof
of subject reduction
of the lambda-calculus.
- Finally, the code for a 2-level proof
of type preservation of a continuation machine with a ordered linear SL.
- 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.