Tinkering with the mathematical foundations of logic and computation
I am a graduate student in the Computer Science Department at Carnegie Mellon University, where I am studying for a PhD in Pure and Applied Logic, advised by Frank Pfenning. My undergraduate studies were at Merton College, University of Oxford, where I obtained a BA in Computer Science and Philosophy.
I am principally interested in the design and analysis of formal/computational systems – i.e. programming languages, logical frameworks, automated theorem provers, etc. – that enable and enhance the production and organization of human knowledge and expression. Toward this end, the central aim of my research is to develop a greater understanding of the abstract, mathematical principles that underlie such systems, using concepts and methods from category theory, type theory, and mathematical logic. For those interested, more detail about the overarching themes of my work can be found here.
My personal wiki and digital garden – The Hyrax Project – is an online formalization project, written in Agda, that serves as a public repository for my thoughts on all things computational, mathematical, and philosophical, with a particular emphasis on categorical logic, type theory, and synthetic mathematics.
In a former life, I was an aspiring composer, and I still spend much of my spare time writing music; you can find a selection of my compositions here.
