Proving Correctness of Modular Functional Programs
One reason for studying and programming in functional
programming languages is that they are easy to reason about, yet
there is surprisingly little work on proving the correctness of
large functional programs. In this dissertation I show how to
provide a system for proving the correctness of large programs
written in a major functional programming language, ML. ML is split
into two parts: the Core (in which the actual programs are
written), and Modules (which are used to structure Core programs).
The dissertation has three main themes:
- Due to the detail and complexity of proofs of programs, a
realistic system should use a computer proof assistant, and so I
first discuss how such a system can be coded in a generic proof
assistant (I use Paulson's Isabelle).
- I give a formal proof system for proving properties of programs
written in the functional part of Core ML.
- The Modules language is one of ML's strengths: it allows the
programmer to write large programs by controlling the interactions
between its parts. In the final part of the dissertation I give a
method of proving correctness of ML Modules programs using the
well-known data reification method. Proofs of reification using
this method boil down to proofs in the system for the Core.
This report is available in the following formats: