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@haskell.org http://www.haskell.org/mailman/listinfo/haskell