MPhil/Part III Projects



Quotients, Inductive Types, & Quotient Inductive Types

  • Supervisors: Marcelo Fiore and Andrew Pitts

  • Background: Type theory and category theory.

  • Topic: The paper Quotients, Inductive Types, & Quotient Inductive Types introduces an expressive class of (indexed) quotient-inductive types as initial algebras for (indexed) families of equational theories and, by means of categorical methods, proves that they can be derived from quotient types and inductive types in a suitable extensional type theory.

  • Project: To immerse yourself into the research area of the paper, studying and presenting it in a dissertation, and possibly pursuing research directions as indicated in its conclusion.



  • Formal Metatheory of Second-Order Abstract Syntax

  • Supervisors: Marcelo Fiore and Dmitrij Szamozvancev

  • Background: Type theory and category theory.

  • Topic: The paper Formal Metatheory of Second-Order Abstract Syntax presents a categorically-inspired language formalisation framework implemented in Agda. The system translates the description of a syntax signature with variable-binding operators into an inductive, intrinsically-encoded data type equipped with syntactic operations along with their correctness properties. The generated metatheory further incorporates metavariables and their associated operation of metasubstitution, which enables second-order equational/rewriting reasoning.

  • Project: To immerse yourself into the research area of the paper, studying and presenting it in a dissertation, while using and/or extending the system in applications, possibly pursuing research directions as indicated in its conclusions.