Imperial College London

ProfessorPhilippaGardner

Faculty of EngineeringDepartment of Computing

Professor of Theoretical Computer Science
 
 
 
//

Contact

 

+44 (0)20 7594 8292p.gardner Website

 
 
//

Location

 

453Huxley BuildingSouth Kensington Campus

//

Summary

 

Models of Computation - CO240

Aims

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

Role

Course Leader

Separation Logic: Scalable Reasoning about Programs - CO404

Aims

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.

The theoretical part of the course will revolve around a simple While language, whereas the practical part will touch on real-world languages such as Java, JavaScript and C.

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.

Role

Course Leader