Thanks for all the replies I got, they have been helpful!
Cheers,
Gerwin
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
Gerwin - I did some work on this a number of years ago for the related
language Miranda. This builds on logical renderings of Haskell (and also
Miranda). The translations are reported in
A Logic for Miranda, Revisited. Simon Thompson. Formal Aspects of
Computing, (7), March 1995.
Simon Thomps
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 f
gerwin.klein:
> 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.
Hey Gerwin,
On
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
_
