My current research interests are in ordinal analysis and non-wellfounded proof theory. It has been observed by a couple of proof theorists that the the notions of proof appearing in each field are closely related, and most of what I do now is try to make this observation more explicit.

I am also interested in type theory, especially in relation to proof theory although I am not working on any such projects.

Research Projects

Cyclic proofs for $\beta$-logic

In the paper Dilator-based analysis of KP, H. Jeon develops a non-wellfounded system for $\beta$-logic. I have defined a regular fragment of the base system and am investigating its proof-theoretic properties.

Ranking Non-wellfounded Proofs by Dilators

One such way the two notions of proofs should be related is that non-wellfounded proofs should be rankable by dilators. This has already appeared in some form in the literature but has not been broadly applied. In collaboration with a co-author, we are working on carrying this out for many systems.

Writing

The Analogy Between Inductively-defined Sets and Computably Enumerable Sets

There is a clear analogy between the construction of inductive sets from below and c.e. sets. I wanted to make this formally precise and stumbled across some old results that do all the work.