[Haskell] translating Haskell into theorem provers

[S.J.Thompson]

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 Thompson: Formulating Haskell. in John Launchbury, Patrick M. Sansom
(Eds.): Functional Programming, Glasgow 1992, Proceedings of the 1992
Glasgow Workshop on Functional Programming, Ayr, Scotland, 6-8 July 1992.
Workshops in Computing Springer 1993, ISBN 3-540-19820-2


The work on Isabelle is reported in

Miranda in Isabelle. Steve Hill and Simon Thompson. In Lawrence C.
Paulson, editor, Preceedings of the first Isabelle Users Workshop, number
397 in University Of Cambridge Computer Laboratory Technical Reports
Series, pages 122-135, September 1995


Regards

Simon




On Wed, 1 Mar 2006, 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
>