Unit information: Types and Lambda Calculus in 2020/21

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
Pre-requisites	COMS10003 Mathematical Methods for Computer Scientists or MATH10004 Foundations & Proof COMS11700 Theory of Computation COMS10006 Functional Programming COMS22201 Language Engineering
Co-requisites	None
School/department	Department of Computer Science
Faculty	Faculty of Engineering

Description including Unit Aims

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 Information

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

Assessment Information

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.