# 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