[Haskell-cafe] Re: Verifying Haskell Programs

[Stefan Monnier]

> State of the art is translating subsets of Haskell to Isabelle, and
> verifying them. Using model checkers to verify subsets, or extracting
> Haskell from Agda or Coq.

Another state of the art is to use type classes, GADTs, and/or type
functions, to specify and prove the properties you want about
your program.  Basically using similar techniques as used in dependently
typed languages.


        Stefan