Christina O'Donnell
,
Contact
Research Summary
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
Current Research
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.
Past Research
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.