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 Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell