Lectures on Constructive Functional Programming

Abstract

The subject of these lectures is a calculus of functions for deriving programs from their specifications. This calculus consists of a range of concepts and notations for defining functions over various data types (including lists, trees and arrays), together with their algebraic and other properties. Each lecture begins with a specific problem, and the theory necessary to solve it is then developed. In this way we hope to show that a functional approach to the problem of systematically calculating programs from their specifications can take its place alongside other methodologies.