[Haskell-cafe] Proving programs

[Simon Thompson]

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

  http://www.cs.kent.ac.uk/people/staff/sjt/Pubs/ProofChapter.pdf

I hope that you find it useful.

Kind regards

Simon


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