[Haskell] formal verification for functional programming languages

[Till Mossakowski]

Wolfgang Jeltsch wrote:
> Hello,
> 
> where can I find information about formal verification techniques and tools 
> for functional programming languages?  Both introductionary texts and current 
> research papers etc. are welcome.

See the specification language HasCASL. For specification of monadic
programs, we have developed a Hoare calculus and a dynamic logic,
which are also represented in the theorem prover Isabelle.
Related is the Heterogeneous Tool Set.

http://www.tzi.de/agbkb/forschung/formal_methods/CoFI/HasCASL/
http://www.tzi.de/cofi/hets

The Isabelle tutorial has some examples from functional programming

http://www4.in.tum.de/~nipkow/LNCS2283/

Also, P-logic and the Programatica tool should be of interest:

ftp://ftp.cse.ogi.edu/pub/pacsoft/papers/Plogic.pdf
http://www.cse.ogi.edu/PacSoft/projects/programatica/

Greetings,
Till

-- 
Till Mossakowski               Phone +49-421-218-4683
Dept. of Computer Science      Fax +49-421-218-3054
University of Bremen           till at tzi.de
P.O.Box 330440, D-28334 Bremen http://www.tzi.de/~till