Re: [Haskell] 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.

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