Message-ID: <436DA5BA.6010002@bawi.org>
Date: Sat, 05 Nov 2005 22:42:02 -0800
From: "Ahn, Ki-yung" <kyagrd@bawi.org>
User-Agent: Thunderbird 1.5 (Windows/20051025)
MIME-Version: 1.0
To: Haskell ML <haskell@haskell.org>
Subject: Re: [Haskell] formal verification for functional programming
 languages
References: <200511041213.04185.wolfgang@jeltsch.net>
In-Reply-To: <200511041213.04185.wolfgang@jeltsch.net>
Content-Type: text/plain;
  charset=ISO-8859-1;
  format=flowed
Content-Transfer-Encoding: 7bit
Precedence: list
Sender: haskell-bounces@haskell.org
Errors-To: haskell-bounces@haskell.org

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
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell