Unit information: Types and Lambda Calculus (Teaching Unit) in 2024/25

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
Units you must take before you take this one (pre-requisite units)

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.

Units you must take alongside this one (co-requisite units)

COMS30081 Topics in Computer Science (Exam assessment unit, 20 credits).

Units you may not take alongside this one

None

School/department School of Computer Science
Faculty Faculty of Engineering

Unit Information

Why is this unit important?

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.

How does this unit fit into your programme of study?

This is an optional unit that can be taken in year 3.

Your learning on this unit

An overview of content

In this unit we will study the following topics:

  • Mathematical proof, and writing proofs as a form of programming
  • Syntax and semantics of an untyped lambda calculus
  • Meta-theory of an untyped lambda calculus
  • Type systems: types, judgements and rules
  • Correspondence between (constructive) proofs and (typed) programs

The emphasis is on precise definitions and developing the theory by writing proofs.

How will students, personally, be different as a result of the unit

Students will have developed a sharper understanding of logical arguments and have a keener sense for when arguments, throughout life, are flawed or otherwise what assumptions they depend on. In computer science, they will understand more deeply the foundations of programming languages, and thus be able to easily assimilate new and cutting-edge programming language features that they may encounter in a future career and stand out from their colleagues as an expert in the subject.

Learning Outcomes

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

  1. Construct terms to illustrate features of the semantics
  2. Prove properties of specific terms and about the existence of terms
  3. Prove that terms are or are not typable
  4. Prove properties of a type system

How you will learn

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.

How you will be assessed

Tasks which help you learn and prepare you for summative tasks (formative):

Weekly problem sheets, with student answers marked by teaching staff, example solutions and tutorial-style problem classes.

Tasks which count towards your unit mark (summative):

This will contribute 50% to the 20cp Topics in Computer Science exam (equivalent to 1 hour of exam time) that will be sat during the winter examination period. This exam will assess ILOs 1-4.

When assessment does not go to plan

Students will retake relevant assessments in a like-for-like fashion in accordance with the University rules and regulations.

Resources

If this unit has a Resource List, you will normally find a link to it in the Blackboard area for the unit. Sometimes there will be a separate link for each weekly topic.

If you are unable to access a list through Blackboard, you can also find it via the Resource Lists homepage. Search for the list by the unit name or code (e.g. COMS30040).

How much time the unit requires
Each credit equates to 10 hours of total student input. For example a 20 credit unit will take you 200 hours of study to complete. Your total learning time is made up of contact time, directed learning tasks, independent learning and assessment activity.

See the University Workload statement relating to this unit for more information.

Assessment
The assessment methods listed in this unit specification are designed to enable students to demonstrate the named learning outcomes (LOs). Where a disability prevents a student from undertaking a specific method of assessment, schools will make reasonable adjustments to support a student to demonstrate the LO by an alternative method or with additional resources.

The Board of Examiners will consider all cases where students have failed or not completed the assessments required for credit. The Board considers each student's outcomes across all the units which contribute to each year's programme of study. For appropriate assessments, if you have self-certificated your absence, you will normally be required to complete it the next time it runs (for assessments at the end of TB1 and TB2 this is usually in the next re-assessment period).
The Board of Examiners will take into account any exceptional circumstances and operates within the Regulations and Code of Practice for Taught Programmes.