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 till@tzi.de P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till