[Haskell] translating Haskell into theorem provers

Donald Bruce Stewart dons at cse.unsw.edu.au
Wed Mar 1 02:41:36 EST 2006

> 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.


This paper also has some references to other work in Haskell.  Perhaps
the Agda people can explain further?

-- Don

More information about the Haskell mailing list