MMath Mathematics and Statistics

Programming languages provide abstractions such as `functions’ which are supposed to allow us to reason about the code at a high level---without running it in our heads. However, these abstractions don’t necessarily behave in the way their names suggest.

In this unit we show that a mathematical theory of program meanings can be developed which encompasses the counter-intuitive behaviour of computations, but preserves our ability to reason abstractly. The machinery required is significant, and delicate at times, and the unit will introduce the fundamental technical tools which help us cope with these complications.

COMP31311 pre-requisites are MATH11121 or COMP11120

COMP11120 or MATH10111
 

This unit aims to equip students to participate in technical discussion of high-level programming language features, covering the core concepts which underpin contemporary developments. It makes the case that questions about what programs mean ought to be posed and settled on the basis of rigorous mathematics, and gives a sense of what has been achieved in this area.  This unit is a good choice for those who want to understand programming languages at a deep level; it also provides a solid foundation for work or further study in the field. 

ILO 1: apply fundamental theoretical results about programming languages and particular techniques to reason about programs;

ILO 2: compute the denotations of types and programs;

ILO 3: prove equivalence of programs in a suitable programming language making use of appropriate techniques and models;

ILO 4: prove selected results about programs using structural induction;

ILO 5: describe and analyse the behaviour of programs in the various models of computation studied;

This unit aims to equip students to participate in technical discussion of high-level programming language features, covering the core concepts which underpin contemporary developments. It makes the case that questions about what programs mean ought to be posed and settled on the basis of rigorous mathematics, and gives a sense of what has been achieved in this area.  This unit is a good choice for those who want to understand programming languages at a deep level; it also provides a solid foundation for work or further study in the field.

On this unit we look at three formal systems, with increasingly sophisticated features, to give examples of suitable reasoning principles. The untyped lambda calculus is a  system that captures computation by rewriting terms. The key feature is the distinction between free and bound variables, and that of capture-avoiding substitution which ensures that we don't rewrite indiscriminately. This system is powerful, but not very intuitive, and easily allows us to write terms that don't seem to make much computational sense. In the simply typed lambda calculus a type system is imposed to rule out such terms. This turns out to give us a system that lacks computational power, and we put that back to obtain the system PCF which may be viewed as the core of modern functional languages. Introducing more sophisticated features in stages allows us to introduce notions as they become useful, and we are able to see them at work in different systems.

As programmers, we might want to think of two programs serving the same purpose (or being equivalent) if, whenever we may use one of them in a larger program, we might as well use the other without being able to detect any difference in the behaviour of the larger program. This is known as contextual equivalence, but it is hard to reason about using only syntax. We introduce the notion of a denotational semantics to allow us to reason about mathematical entities instead, and we investigate what properties such a semantics needs in order to allow us to reason about our terms. We provide models for the two more sophisticated systems and study their properties.

We also introduce the notion of logical relation as a powerful proof method.

The unit is based on detailed lecture notes including numerous exercises. They go beyond the material we assess by providing rigorous arguments for all the results given, as well as the relevant mathematical background. The notes are supported by videos that explain key concepts and ideas.

The approach to learning is blended: Key ideas are explored by the learners via introductory activities in the workshops, with support from unit staff, and plenary discussions take place to confirm the learners’ understanding and to correct any misconceptions. This prepares the students for the directed reading, supported by short videos, for the week. Students are asked to carry out formative exercises and they receive feedback via solutions that are released the following week.

There are coursework exercises in the form of take home tests which assess all ILOs, but only cover the first two languages taught. Further exercises are made available to prepare students for the questions they can expect for the exam.

 

Feedback is provided in a number of ways, via the self-assessment quizzes, via solutions provided for unassessed exercises, via the weekly study sessions where students can query their understanding, and via feedback provided on the two pieces of coursework.