,
My present research is in the semantics of Quotient Inductive-Inductive Types (QIITs), a kind of inductive type with an explicit equality relation (quotient) given by path constructors. I am… read more
My present research is in the semantics of Quotient Inductive-Inductive Types (QIITs), a kind of inductive type with an explicit equality relation (quotient) given by path constructors. I am presently interested in constructing QITs in a way that avoids all choice. Type theory is a constructive approach of logic, meaning all existence claims (∃ x s.t. P(x)) may only be satisfied by an explicit witness: (x , p) where p is a proof of P(x). This differs from classical logic, in which statements such as 'P or not P' are assumed a priori. Type theories play a foundational role in the formalisation of logical proofs -- the effort to verify the correctness of mathematical proofs using computer-aided verification. This is useful in verifying mathematical proofs, as well as proving safety properties of software systems. The research goal is the formalization of a type theory that can represent the syntax and semantics of other type theories (and itself, i.e. self-hosting). Significant progress has been made toward in this goal past 10 years, through the use of 'quotient inductive-inductive types', which are a combination of the following: - quotient inductive types: types made from one of a set of certain constructors which allow for an arbitrary identification of types up to the one used by the type system. - inductive-inductive types: a way of defining inductive types simultaneously, e.g. a types A and B can be constructed even when B is indexed by A and A may refer to constructors involving B. The aim is to help in developing a type theory that admits universal and possibly infinitary QIITs, ensuring consistency, self-hosting, and non-reliance on non-constructive proofs. Most of my work takes place mainly within Agda, a proof assistant based on type theory.
MSc Thesis: Virtual Sets as a Traced Monoidal Category (2025) University of Nottingham Supervisor: Prof. Thorsten Altenkirch
Formalised a category of finite injective functions ("Virtual Sets") using Cubical Agda.
Established the monoidal structure of the category.
Investigated the axioms required for a Traced Monoidal Category.
Identified structural barriers in indexed inductive Fin types due to excessive transport complexity.
Concluded that a Two-Level Type Theory (2LTT) approach is required to make coherence conditions for strict equality tractable.
Independent Research: Semantic Graph Rewriting (2023-2025)
Developed a formal system for representing programming language syntax and semantics using graph theory.
Designed a graph reduction system to handle variable binding and substitution, as a comparative study against standard type-theoretic approaches.
Formalised operational semantics via custom rewrite rules to explore self-descriptive logic.
The University of Nottingham School of Computer Science Jubilee Campus Nottingham, NG7 1BB
telephone: +44 (0) 115 95 14220 email:fp-lunch@cs.nott.ac.uk