The Heterogeneous Tool Set supports HasCASL for specification of Haskell programs, and uses Isabelle for proving http://www.dfki.de/sks/hets
Moreover, the Programatica project has an expressive logic called P-logic, and tools supporting it: http://programatica.cs.pdx.edu/ Best, Till Am 25.10.2010 10:09, schrieb Romain Demeyer:
Hello, I'm working on static verification in Haskell, and I search for existing works on specification of Haskell programs (such as pre/post conditions, for example) or any other functional language. It would be great if there exists a prover based on this kind of specifications. I already found the ESC/Haskell. Do you know some other works which could be interesting? Thanks, rde. _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
