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 | 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.

Upon successful completion 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 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.

January timed assessment (100%, 10 credits)

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

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