Email Gateway (Aug 18 2022 at 15:04): Email Gateway (Aug 18 2022 at 15:04):From: Peter Lammich <peter.lammich@uni-muenster.de>
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
Email Gateway (Aug 18 2022 at 15:06):From: Lukas Bulwahn <bulwahn@in.tum.de>
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,
Lukas
Peter Lammich wrote:
Last updated: Apr 19 2024 at 20:15 UTC