My current research intersts are in ordinal analysis and cyclic proof theory, especially from a categorical perspective.

Research Projects

Proof Systems for $\beta$-logic

I have been thinking about proof systems for Girard's $\Pi^1_2$-logic.

Cyclic Proofs and Ordinal Traces

This project studies cyclic and non-wellfounded proof systems whose soundness is controlled by progressing traces. I am especially interested in analogues of trace conditions for proof systems involving ordinal parameters.

Dilators

Dilators are a higher type functorial notion of ordinal introduced by J.-Y. Girard in the context of ordinal analysis. They are $\Pi^1_2$-complete and so can be used to measure the $\Pi^1_2$ consequences of a theory. I am currently thinking about the categorical structure of dilators and their categorical properties.

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. </details>