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 |
| 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:
- Describe functions using lambda notation and calculate using the beta rule.
- Argue that lambda terms satisfying given properties do or do not exist.
- Argue that given properties of lambda terms are or are not decidable.
- Construct derivations of typing judgements to show that terms are well typed.
- Identify systems for which principal types exist and construct principal types for terms.
- Organise type systems by their expressive power and the computability of inference.
- Explain the role of lambda calculus and formal type systems as a foundation for modern programming languages.
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.
