Lecture-33 hours
Supervised time in studio/workshop-22 hours
Guided independent study-145 hours Total: 200 hours
Exclusions
Description
This module builds on the Logic and Computation module, introducing students to the concept of types, core to the design of modern functional programming languages. The use of types ranges from giving a high level of control over the way a program interacts with its environment (monads) to providing an alternative foundation of mathematics which is particularly suited to reasoning about programs (dependent types). This module introduces students to type theory, type systems, and their applications to the design of modern functional programming languages. In addition, students will learn about practical applications of types to control effects via monads and manage polymorphism via type classes. Using dependent type systems students will be introduced to the theory and practice of program certification.
Learning Outcomes
By the end of the module students should be able to:
Write programs involving infinite data structures.
Write functional programs using advanced features such as type classes and monads.
Write formal proofs of correctness of programs using dependent type theory.
Understand the Curry-Howard correspondence between logic and type theory.