[Haskell] translating Haskell into theorem provers
Donald Bruce Stewart
dons at cse.unsw.edu.au
Wed Mar 1 02:41:36 EST 2006
> is any of you aware of activities that aim to translate Haskell into
> interactive theorem provers like PVS or Isabelle/HOL? (automatically or
> We know about the Programatica project and Brian Huffman's work, but turned
> up little else.
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
This paper also has some references to other work in Haskell. Perhaps
the Agda people can explain further?
More information about the Haskell