*Lecturer: Dr A. Dawar*
(`ad260@cl.cam.ac.uk`)

*No. of lectures:* 12

**Aims**

The aims of the course are to introduce the principles of functional programming using the programming language ML. The course will illustrate the principles using key features of ML, including structured datatypes, higher order functions and type-checking. Applications of these will be demonstrated through a series of case studies.

**Lectures**

**Overview and motivation.**Imperative commands*versus*functional expressions. Evaluation strategies: call-by-value, call-by-name, call-by-need. Lazy evaluation.**Introduction to Standard ML.**Basic types: integers, reals, strings, Booleans. Structured types: tuples, lists, functions.**Lists and recursion.**Functions on lists: length, reverse, append. Recursion*versus*iteration. Utilities.**Basic sorting.**Equality types. Sorting lists using quicksort and merge sort.**Datatypes.**Enumerated types. Pattern matching. Raising and handling exceptions. Binary trees; computing size and depth, traversing, balancing. Multi-branching trees, S-expressions.**Further datatypes.**Binary search trees. Functional arrays. Propositional logic: negation normal form, conjunctive normal form.**Higher order functions.**Higher-order functions. Lambda-notation. Curried functions. Functionals: list summation, map, matrix multiplication, list folding.**Higher order functions continued.**Unbounded sequences. Consuming and joining sequences. Functionals on sequences. Numerical computations. Searching infinite trees.**Program specification and verification.**Testing*versus*program verification. Formal*versus*rigorous proof. Proofs of ML programs. Mathematical and course-of-values induction.**Induction.**Structural induction on lists. Proofs of appending and reversing. Structural induction on trees. Specification of sorting.**Types.**ML type inference. Polymorphism: types and type schemes. Axioms and inference rules.**Case study: a functional parser.**Parsing functionals: alternation, sequencing, transformation, repetition. Example: propositional logic.

**Objectives**

At the end of the course students should

- be able to develop software in ML in a competent manner
- be familiar with key concepts of programming in a recursive,
functional style
- understand how to use type-checking for clearer and verifiable
programs

**Recommended books**

Paulson, L.C. (1996). *ML for the Working Programmer*. Cambridge
University Press (2nd ed.).

Other useful references:

Backus, J. (1978). Can programming be liberated from the von Neumann
style? A functional style and its algebra of programs. *Communications of the ACM*, vol. 21, pp. 613-641.

Barendregt, H.P. (1984). *The Lambda Calculus: its Syntax and
Semantics*. North-Holland.

Landin, P.J. (1966). The next 700 programming
languages. *Communications of the ACM*, vol. 9, pp. 157-166.