translating Haskell into theorem provers

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

translating Haskell into theorem provers

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.

Cheers,
Gerwin

_______________________________________________
Haskell mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell
Reply | Threaded
Open this post in threaded view
|

Re: translating Haskell into theorem provers

Donald Bruce Stewart
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
_______________________________________________
Haskell mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell
Reply | Threaded
Open this post in threaded view
|

Re: translating Haskell into theorem provers

Till Mossakowski
In reply to this post by Gerwin Klein
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
> [hidden email]
> 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           [hidden email]
P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till
_______________________________________________
Haskell mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell
Reply | Threaded
Open this post in threaded view
|

Re: translating Haskell into theorem provers

Simon  Thompson
In reply to this post by Gerwin Klein



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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell
>
_______________________________________________
Haskell mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell
Reply | Threaded
Open this post in threaded view
|

Re: translating Haskell into theorem provers

Gerwin Klein
Thanks for all the replies I got, they have been helpful!

Cheers,
Gerwin
_______________________________________________
Haskell mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell