[Haskell-cafe] Proving programs

Simon Thompson s.j.thompson at kent.ac.uk
Wed Jan 2 18:22:54 CET 2013

Christopher, there's an introduction to proof for functional programs at


I hope that you find it useful.

Kind regards


On 1 Jan 2013, at 23:24, Christopher Howard <christopher.howard at frigidcode.com> wrote:

> 1. Does this approach need to be adjusted for a functional language, in
> which computation is (at least idealistically) distinct from control flow?
> 2. How do we approach this for programs that have an input loop (or
> recursion)? E.g., I have an application that reads one line for stdin,
> modifies said line, outputs to stdout, and repeats this process until
> EOF? Should I be thinking of every iteration as a separate program?

Simon Thompson | Professor of Logic and Computation 
School of Computing | University of Kent | Canterbury, CT2 7NF, UK
s.j.thompson at kent.ac.uk | M +44 7986 085754 | W www.cs.kent.ac.uk/~sjt

More information about the Haskell-Cafe mailing list