There is a prototype translation of Haskell to Isabelle/HOL and
Isabelle/HOLCF written by Paolo Torrini. Unlike the Programatica
translation, it uses a shallow encoding of the type system. Constructor
classes (not available in Isabelle) are translated using theory
morphisms. Programatica is used for parsing and type checking.
The translation is part of the heterogeneous tool set (Hets) [1],
but currently works only in a standalone version, called h2hf. You can
compile h2hf from the Hets sources with "make h2hf". Since there is
interest, we will provide a website with binaries, explanation and
examples soon.
Greetings,
Till
[1] http://www.tzi.de/cofi/hets
Gerwin Klein wrote:
Hi,
is any of you aware of activities that aim to translate Haskell into
interactive theorem provers like PVS or Isabelle/HOL? (automatically or
manually).
We know about the Programatica project and Brian Huffman's work, but turned
up little else.
Cheers,
Gerwin
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
--
Till Mossakowski Phone +49-421-218-4683
Dept. of Computer Science Fax +49-421-218-3054
University of Bremen [EMAIL PROTECTED]
P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
