[Haskell-cafe] Re: Verifying Haskell Programs

Stefan Monnier monnier at iro.umontreal.ca
Mon Feb 2 22:14:48 EST 2009

> 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.


More information about the Haskell-Cafe mailing list