On Nov 4, 2005, at 3:13 AM, 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.

Best wishes, Wolfgang

Please do consider posting a summary of responses you receive. I'm looking for much the same type of information. If it's of any value, two books I'm reading right now are Benjamin C. Pierce, "Types and Programming Languages" Klaus Schneider, "Verification of Reactive Systems: Formal Methods and Algorithms" I still don't think I understand how to apply these ideas in a useful way, but a book I picked up a couple of years ago and found absolutely fascinating (possibly what led me down the path of exploring functional programming, believe it or not) is David Harel, Dexter Kozen and Jerzy Tiuryn, "Dynamic Logic" Pierce is part of a two volume series, and focuses on typed lambda calculus, with implementation examples in ML. (I just hope the syntax doesn't throw a Haskell newbie like me off too much!) Schneider has a bit more of a handbook feel to it, but focuses on automata based methods and their relationship with *temporal* logic. I've just started reading it, but it doesn't seem to be particularly functional, but seems interesting. Kozen et al. is an introduction to dynamic logic, a modal program logic generalizing Hoare's invariant logic (pre- and post-conditions. The idea of DL is to interpret [P]a to mean a must hold after an execution of P and <P>a to mean that it holds after some execution of P. The logic becomes interesting when the semantics of [P] and <P> for composite programs are given in terms of those of their subprograms. What is intriguing is that it is possible to prove decidability based on "small model" properties which are somewhat surprising, since the proof of compactness for traditional logic doesn't carry though at all. I am still looking for somewhat more satisfying account of lambda calculus, though. It is frustrating to read that there is this mysterious result called the Church-Rosser theorem stating that the order in which you reduce a lambda expression doesn't affect the normal form you (may) reach. I often wonder if this kind of mystery is a lot of what leads people to shy away from functional programming, given that lambda calculus seems a lot harder to understand on an intuitive level than Turing machines or RAMs (which are appropriate models for procedural programming). === Gregory Woodhouse gregory.woodhouse@sbcglobal.net "Einstein was a giant. He had his head in the clouds and his feet on the ground." --Richard P. Feynman

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