> 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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
