[Haskell] translating Haskell into theorem provers

[Till Mossakowski]

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