Skip to main content

Unit information: Types and Lambda Calculus in 2019/20

Please note: Due to alternative arrangements for teaching and assessment in place from 18 March 2020 to mitigate against the restrictions in place due to COVID-19, information shown for 2019/20 may not always be accurate.

Please note: you are viewing unit and programme information for a past academic year. Please see the current academic year for up to date information.

Unit name Types and Lambda Calculus
Unit code COMS30009
Credit points 10
Level of study H/6
Teaching block(s) Teaching Block 1 (weeks 1 - 12)
Unit director Dr. Steven Ramsay
Open unit status Not open

COMS10003 Mathematical Methods for Computer Scientists or MATH10004 Foundations & Proof

COMS11700 Theory of Computation

COMS10006 Functional Programming

COMS22201 Language Engineering



School/department Department of Computer Science
Faculty Faculty of Engineering


Type systems are one of the most basic tools at the disposal of programmers in their daily work, and the underlying theory is one of the richest in computer science. This unit provides an introduction to this theory by studying its formalisation in the lambda calculus.

Intended learning outcomes

By the end of the unit students will be able to:

  • Recall the fundamental definitions and theorems of the lambda calculus.
  • Illustrate the theory by implementing examples and constructing precise mathematical arguments.
  • Apply the theory to the analysis of programming languages and their type systems.

Teaching details

20 lectures; problem classes. One drop-in session per week.

Assessment Details

2-hour written exam (100%)

Reading and References

There is no required reading, but the following are useful references:

  • H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics. College Publications, 2012.
  • J. R. Hindley and J. P. Seldin. Lambda Calculus and Combinators: An Introduction. Cambridge University Press, 2008.
  • B. C. Pierce. Types and Programming Languages. MIT Press, 2002.
  • H. P. Barendregt, W. Dekkers and R. Statman. Lambda Calculus with Types. Cambridge University Press, 2013.