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
_______________________________________________
Haskell mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell
