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.