Hello, welcome to my little corner of the internet! I’m Christina O’Donnell, I’m a PhD student in theoretical computer science at the University of Nottingham supervised by Thorsten Altenkirch. I work mainly on type theory, quotient inductive types, and constructive foundations, with a particular interest in how formal systems can describe their own syntax and semantics.
News
- 2026-05-04: Talk at TYPES 2026: “Constructing QITs from Quotients”.
Research Interests
- Type Theory
- Quotient Inductive Types
- Quotient Inductive-Inductive Types
- Constructive Mathematics
- Agda
- Categorical Logic
Current Research
My current research concerns the semantics of quotient inductive-inductive types (QIITs). These are a form of inductive definition that allows several types to be generated simultaneously, while also imposing equations between generated objects.
I am particularly interested in when such types can be constructed without appealing to non-constructive principles such as the Axiom of Choice. This matters because type theory is often used as a constructive foundation: an existence proof should provide an explicit witness, rather than merely showing that a witness cannot fail to exist.
A motivating goal is to understand the foundations needed to formalise type theories inside type theory itself. QIITs are important here because they provide a way to define syntax, typing judgments, substitution, and equality simultaneously. Much of my work is carried out in Agda, a proof assistant based on dependent type theory.
Academic and Professional Background
- PhD in Computer Science, University of Nottingham, 2025–present.
Supervised by Thorsten Altenkirch. Funded by an EPSRC Doctoral Landscape Award. - MSc in Computer Science, University of Nottingham, 2024–2025.
- Computer Science Tutor, 2023–2024.
- Software Developer, Cyberscience, 2017–2023.
- BA in Mathematics and Computer Science, University of Oxford, 2014–2017.
Selected Projects
MSc Thesis: Virtual Sets as a Traced Monoidal Category
In my MSc thesis, supervised by Thorsten Altenkirch, I formalised a category of finite injective functions, called Virtual Sets, inspired by the work of Mark Williams, using Cubical Agda. I established its monoidal structure and investigated the additional structure required for a traced monoidal category.
The project also exposed practical difficulties caused by transport-heavy indexed inductive definitions, which led me toward thinking about strict equality, coherence, and two-level type theory.
Semantic Graph Rewriting
Before my PhD, I worked on a graph-based approach to representing programming language syntax and semantics. The aim was to model binding, substitution, and operational semantics using graph rewriting, as an alternative perspective on self-descriptive formal systems.
Formalisation
Most of my formalisation work is in Agda, including work with Cubical Type Theory, categorical structures, quotient inductive types, and setoid-based semantics.
Contact
Email: christina@octocurious.com
You can also find me on:
- GitHub: https://github.com/cdo256
- This website: https://octocurious.com