[Haskell] 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