Skip to navigation | Skip to main content | Skip to footer
Menu
Menu

COMP31311 Giving Meaning to Programs syllabus 2021-2022

COMP31311 Giving Meaning to Programs

Level 3
Credits: 10
Enrolled students: 17

Course leader: Andrea Schalk


Additional staff: view all staff

Requisites

  • Pre-Requisite (Compulsory): MATH10111
  • Pre-Requisite (Compulsory): COMP11120

Additional requirements

  • COMP11120 or MATH10111

Assessment methods

  • 80% Written exam
  • 20% Practical skills assessment
Timetable
SemesterEventLocationDayTimeGroup
Sem 1 w1-5,7-12 ONLINE ACTIVITY Mon 16:00 - 17:00 -

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

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.

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 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.

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

  • Lectures (11 hours)

Employability skills

  • Analytical skills
  • Innovation/creativity
  • Problem solving

Learning outcomes

On successful completion of this unit, a student will be able to:

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

  • Prove equivalence of programs in a suitable programming language

  • Apply fundamental theoretical results about programming languages to reason about terms

  • Compute the denotations of programs and types

  • Explain the importance of contextual equivalence and its relationship to fully abstract semantics

Reading list

No reading list found for COMP31311.