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
Pre-requisites	COMS10016 Imperative and Functional Programming or equivalent. COMS10014 Mathematics for Computer Science A or equivalent. COMS20007 Programming Languages and Computation or equivalent. or 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.
Co-requisites	COMS30039 Types and Lambda Calculus (Exam assessment unit, 10 credits).
School/department	School 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 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 Information

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 Information

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