Computer Laboratory

Part III/MPhil Projects Suggestions

A meta-theory for effectful optimisations

This project aims to establish the meta-theory of effect-dependent source-to-source global compiler optimisations. It builds on the observation that these optimisations arise as algebraic laws for the algebraic description underlying the language’s denotational semantics. Such a meta-theory will enable:

  • a characterisation of which optimisations have such algebraic descriptions;
  • a unification of many existing and tedious proofs for the semantic characterisation of these optimisations;
  • a formulation of practically useful meta-properties of these optimisations; and
  • modular computational models for establishing sound and complete decision procedures within optimising compilers.

This challenging project requires the student to obtain knowledge of categorical semantics of programming languages, the algebraic approach to semantics, and dependently-typed programming.

Pre-requisite knowledge: denotational semantics, and category theory and logic.