Calculating Programs (MGS 2019)

Program calculation is a family of techniques for deriving programs from their specifications. Unlike other approaches, where correctness is verified through proofs or tests that are extrinsic to the program, calculational approaches aim to provide correctness-by-construction, where the correctness of the program follows from the validity of the steps used to produce it.

In this course, we will survey a number of different approaches to calculating programs, all operating at different levels of formality and having differing strengths and weaknesses. We will show how to use these techniques on a number of simple examples, culminating in a longer, more drawn-out example with real-world applicability.

This course assumes a basic knowledge of the principles of functional programming. Other necessary concepts will be introduced as we go.

Lecture 1: Fold/Unfold Calculation

This lecture will cover the fold/unfold style of program calculation, as introduced by Burstall and Darlington.
Slides: pdf keynote

Lecture 2: Programming in Squiggol

This lecture will cover the Bird-Meertens Formalism for calculating programs that operate on lists, also known as "Squiggol".
Slides: pdf keynote

Lecture 3: Fixed Point Calculus

This lecture will cover topics relating to calculating programs as least fixed points, including fixed point induction, fusion and the rolling rule.
Slides: pdf keynote

Lecture 4: Defunctionalisation

This lecture will demonstrate how to apply some of the techniques presented in this course to the problem of defunctionalising an interpreter for a simple language.
Slides: pdf keynote