[Haskell] formal verification for functional programming languages

[Gregory Woodhouse]

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 at sbcglobal.net

"Einstein was a giant. He had his head in the clouds and his feet on  
the ground."
--Richard P. Feynman