Models of Computation - CO240
This module focuses on formal descriptions (models) of computational behaviour. You will learn about:
- the operational semantics (formal description) of a simple 'WHILE' programming language
- the operational semantics of other styles of real-world languages, such as Java and Haskell
- equivalent definitions of algorithm, initiated in the 1930s and providing the foundations for programming languages and computation
Separation Logic: Scalable Reasoning about Programs - CO404
To enable the students to reason compositionally about sequential and concurrent heap-manipulating programs using separation logic, both by exploring the underlying theory and by working with cutting-edge academic and industrial analysis tools. The fact that the reasoning is compositional means that it scales.
More specifically, the students will:
- gain an in-depth understanding of the theory underpinning separation logic, why it works and why it is correct;
- use separation logic to specify and verify sequential programs, focusing on standard data structures and their operations;
- learn how to work with academic and industrial tools based on separation logic;
- gain basic familiarity with concurrent separation logics, in particular their theory and their application to concurrent data-structure algorithms.