[isabelle] Imperative HOL



Hi all,

The TPHOL's 08 paper "Imperative Functional Programming with
Isabelle/HOL" describes some features that
are not contained in the Isabelle2009-1 distribution
(src/HOL/ImperativeHOL).

For example, the datatype definition for a linked list does not work out
of the box,
it gives the error that \alpha node is not in heap-typeclass.

Moreover, there is no implementation of the mentioned MREC-combinator.
Also, I cannot find the described examples (SAT-checker,
Bytecode-verifier) anywhere.

Is there a more complete implementation? Is it available? Are the
examples available?

Regards,
  Peter







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.