BSc Computer Science and Mathematics with Industrial Experience

Year of entry: 2024

Course unit details:
Giving Meaning to Programs

Course unit fact file
Unit code COMP31311
Credit rating 10
Unit level Level 3
Teaching period(s) Semester 1
Available as a free choice unit? Yes

Overview

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.

Pre/co-requisites

Unit title Unit code Requirement type Description
Foundations of Pure Mathematics B MATH10111 Pre-Requisite Compulsory
Mathematical Techniques for Computer Science COMP11120 Pre-Requisite Compulsory

COMP11120 or MATH10111

Aims

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.

Learning outcomes

On the successful completion of the course, students will be able to:

  • Describe and analyse the behaviour of terms in the various models of computation studied

  • Compute the denotations of programs and types

  • Prove selected results about programs using structural induction

  • Apply fundamental theoretical results about programming languages and particular techniques to reason about programs

  • Prove equivalence of programs in a suitable programming language making use of appropriate techniques and models

Syllabus

  • Untyped lambda calculus

  • Simply typed lambda calculus

  • Proof method: logical relations

  • Observational equivalence of programs

  • The function model of the simply typed lambda calculus

  • PCF — the core of modern functional languages

  • Denotational semantics of PCF

  • Taster of advanced topics (perhaps polymorphism or concurrency)

Teaching and learning methods

 

This unit is delivered in a blended manner. Self-study materials are made available in the form of detailed notes which include exercises, as well as videos and formative self-assessment quizzes that allow students to check their understanding. Each week there is a session that allows students to ask questions about the materials and beyond, explore exercises, and discuss the ideas underlying the taught material.

 

Students are expected to spend 4-6 hours per week engaging with the self-study materials, including solving some of the non-assessed exercises. Twice in the semester a significant effort will be required to solve the set coursework.

Employability skills

Analytical skills
Innovation/creativity
Problem solving

Assessment methods

Method Weight
Written exam 80%
Practical skills assessment 20%

Feedback methods

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.

Study hours

Scheduled activity hours
Lectures 11
Independent study hours
Independent study 89

Teaching staff

Staff member Role
Andrea Schalk Unit coordinator

Return to course details