[Haskell] formal verification for functional programming languages
Ahn, Ki-yung
kyagrd at bawi.org
Sun Nov 6 01:42:02 EST 2005
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
More information about the Haskell
mailing list