[Haskell] formal verification for functional programming languages

[Ahn, Ki-yung]

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.

Take a look at Omega. It is an experimental interpreter building up 
Curry Howard Isomorphism within the programming language using 
Generalized Algebraic Data Types.

http://www.cs.pdx.edu/~sheard/Omega/index.html
http://www.cs.pdx.edu/~sheard/papers/OmegaLangOfFutOnwardOct04.ppt
http://www.cs.pdx.edu/~sheard/papers/LangOfTheFuture.ps

If you are familiar with Haskell or want to work on some formal 
verification using Haskell code, I think this one would be convenient 
and also practical since some part of Omega's is already built into GHC 
now. See Generalized Algebraic Data Types section in GHC User Manual.

http://www.haskell.org/ghc/docs/latest/html/users_guide/gadt.html

-- 
   Ahn, Ki Yung