Felix Bradley

My research interests focus on developing and analysing tools and theories for use in formalising foundational mathematics and in the development of new software and programming languages, primarily through the lens of type theory. I'm currently working on the projects in the following areas:

• Coercive Subtyping - Coercive subtyping, whilst useful in proving the soundness and decidability of subtyping, is often hard to reason about and use in applications. I'm currently working on categorical semantics to reason about the properties of type theories with coercive subtyping.
• Subtype Universes - A 'type of subtypes', these were initially suggested as a solution to problems regarding undecidability in bounded quantification. I'm currently working on generalising version of subtype universes and analysing their collective structure in a universe-less theory.
• Pure Subtype Systems - Introduced by DeLesley Hutchins in his PhD thesis, pure subtype systems are akin to a type system with the typing relation replaced with the subtyping relation, and were introduced for programming languages with modules. I'm currently looking at using logical pure subtype systems in proof assistants and enriching them with inductive types.
• Miscellaneous Projects - I'm currently studying developments made in computational homotopy type theory and working on a theory of paths and open sets. I'm also looking at the properties of the programming language Rust and its safety and soundness.

Outside of my research, I also work as a teaching fellow; and as coordinator of the Proofs and Programs Club, an extra-curricular club aimed at teaching undergraduate students the Coq proof assistant and developing their skills in mathematical reasoning and functional programming. I am also currently training for Higher Education Academy associate fellowship and a M-level certificate in education.

Prior to joining the Department of Computer Science at Royal Holloway, I studied mathematics and computer science at the University of Southampton. I graduated with first-class honours, and earned a Dean's List award. My research at Southampton covered aperiodic tilings: teaching analytical tools developed with category theory, and developing new original proofs about localised patterns.