photo of Cory Cory Michael Knapp

School of Computer Science
University of Birmingham
Edgbaston, Birmingham, B15 2TT, UK

I am a PhD student under Martín Escardó. Until May 2015, Paul Blain Levy was a co-supervisor.

My research is on univalent type theory and models of Martin-Löf Type Theory; I'm particularly interested in the relationship between type theory and other topics in constructive math. At present, I'm looking specifically at partial functions and computability theory in univalent type theory. I'm also interested in coalgebras, point-free topology and topos theory; this doesn't mean I know anything about them.

Previously, I did a double BSc in Applied Mathematics and Computer Science at Illinois Institute of Technology, followed by the Barcelona Master in Pure and Applied Logic organized by University of Barcelona. In between, I brewed a lot of coffee.

Slides from a brief (15 minute) talk I gave on homotopy type theory to some other PhD students.

Some agda files


Spring of 2016, I was a TA for Models of Computation.
Fall of 2015, I was a TA for Functional Programming.
In the 2014-15 year, I was a tutor for the Java Workshop which is part of Msc Computer Science.


Martín Escardó and Cory Knapp. Partial Elements and Recursion via Dominances in Univalent Type Theory . Submitted April 2017. pdf

Other stuff

A few PhD students hold "CARGO", a CAtegories Reading GrOup, which meets on Tuesday at 2:00 in room 245. We have a mailing list which you are welcome to subscribe to.

Sometimes I write things about math, or write poems and lyric essays. You can find me on twitter.

Last modified: Wed 25 Aug 13:23 GMT 2016