Re: [Haskell] translating Haskell into theorem provers
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 [EMAIL PROTECTED] P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] translating Haskell into theorem provers
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 ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] translating Haskell into theorem provers
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
[Haskell] 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 ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
