Skip to main content

Unit information: Types and Lambda Calculus (Teaching Unit) in 2020/21

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

COMS10016 Imperative and Functional Programming or equivalent.

COMS10014 Mathematics for Computer Science A or equivalent.

COMS20007 Programming Languages and Computation or equivalent.


Basic set theory, basic logical notation, read and write mathematical proofs, proof by induction, implement functional programs in any functional programming language, decidable vs undecidable problems, draw syntax trees of expressions, read and write types of expressions.


COMS30039 Types and Lambda Calculus (Exam assessment unit, 10 credits).

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 is an introduction to this theory and its presentation through lambda calculi.

Intended learning outcomes

Upon successful completion of the Unit, students will be able to:

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

Teaching details

Teaching will be delivered through a combination of synchronous and asynchronous sessions, including lectures, practical activities supported by drop-in sessions, problem sheets and self-directed exercises.

Teaching will take place over Weeks 1-7, with consolidation and revision sessions in Weeks 11 and 12 for students being assessed by examination.

Assessment Details

January timed assessment (100%, 10 credits)

Reading and References

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

  • Barendregt, Henk P., The Lambda Calculus, its Syntax and Semantics (College Publications, 2012) ISBN: 978-1848900660
  • Hindley, J. Roger and Seldin, Jonathan P., Lambda Calculus and Combinators: An Introduction (Cambridge University Press, 2008) ISBN: 978-1139473248
  • Pierce, Benjamin C., Types and Programming Languages (MIT Press, 2002) ISBN: 978-0262162098
  • Barendregt, Henk P., Dekkers, Wil and Statman, Richard, Lambda Calculus with Types (Cambridge University Press, 2013) ISBN: 978-1139032636