COMP31311 Giving Meaning to Programs syllabus 2021-2022
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
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.
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)
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 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.
- Lectures (11 hours)
- Analytical skills
- Problem solving
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
No reading list found for COMP31311.