Re: [isabelle] Imperative HOL

Hello Peter,

The Linked List example and the MREC combinator are already since December 2009 (changeset 1a82e2e29d67) in the development snapshot.

The Sat-checker and the Bytecode-verifier are still in another repository. If you are interested, we can give you those files. If you want to continue working on those, i.e. the SAT checker would be a perfect example for the new Collection framework (e.g. the clauses are sets implemented by sorted lists at the moment), I would suggest to turn these files into a new AFP entry.

Happy Easter wishes,


Peter Lammich wrote:
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

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?


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