translating Haskell into theorem provers
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
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, One project I can think of is Agda, a theorem prover itself written in Haskell. At last year's Haskell Workshop, there was a paper describing a system that translated Haskell into an Agda model of Haskell, if I recall correctly. http://www.tcs.ifi.lmu.de/~abel/haskell05.pdf This paper also has some references to other work in Haskell. Perhaps the Agda people can explain further? -- Don
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
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
Thanks for all the replies I got, they have been helpful! Cheers, Gerwin
participants (4)
-
dons＠cse.unsw.edu.au -
Gerwin Klein -
S.J.Thompson -
Till Mossakowski