Programs, Proofs and Types
| Code | School | Level | Credits | Semesters |
| COMP4074 | Computer Science | 4 | 20 | Spring UK |
- Code
- COMP4074
- School
- Computer Science
- Level
- 4
- Credits
- 20
- Semesters
- Spring UK
Summary
This module focuses on some of the fundamental mathematical concepts that underlie modern programming and programming languages emphasizing the role of types. We will use a dependently typed programming language / interactive proof system (e.g. Agda) to implement some concepts on a computer.
Example topics include basic lambda calculus, operational semantics, propositions as types and formal verification. You’ll spend around three hours per week in lectures studying for this module and one hour in the lab working with an interactive proof system.
Target Students
Available to Level 3 and Level 4 students in the School of Computer Science. This module is not available to students not listed above without explicit approval from the module convenor(s). This module is part of the Foundations of Computer Science theme in the School of Computer Science.
Assessment
- 50% Coursework 1: Several assessed pieces of coursework. The reassessment for this module will be 100% exam.
- 50% Exam 1 (2-hour): Written exam. The reassessment for this module will be 100% exam.
Assessed by end of spring semester
Educational Aims
To provide a sound basis in a range of topics in the foundations of programming languages, including aspects of recent and current research.Learning Outcomes
Knowledge and Understanding
- A sound understanding of advanced topics in type theory and foundations of programming.
- Being able to apply mathematical methods in Computer Science.
- Being able to use formal methods and formal verification.
- Knowledge of advance programming language concepts.
Intellectual Skills
- The ability to apply mathematical techniques to programming problems.