Jonathan Konig

PhD thesis:

On the Formalization of Type Theories, Species of Structures, and Higher-Order Structures

My PhD research is focused on exploring formalizations in Lean of several related concepts in type theories. The first area will be the development of a fully correct system for producing operational type theories given a binding signature. This system could then be extended to an equational re-writing system for studying equational theories resulting from arbitrary equational presentations. Another area of focus is substructural abstract syntax – type theories which adopt different combinations of axioms for how a variable in context can be used by a term. This research will investigate how to define notions of metavariables and metasubstitution for these type theories, analogous to those of second-order abstract syntax. The final area would be Joyal’s theory of combinatorial species and higher-dimensional category theory. Joyal’s theory provides a calculus for constructing mathematical structures. This research would use constructions involving opetopic shapes to extend a notion of substitution to infinite type theories. 

Who or what inspired you to pursue your research interests?

Curiosity for the fascinating world of abstract mathematical reasoning.