# [Haskell] formal verification for functional programming languages

Gregory Woodhouse gregory.woodhouse at sbcglobal.net
Fri Nov 4 07:51:43 EST 2005

```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
>

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

```