Modal type theory and Higher-dimensional algebra

Research into programming languages and type theory often involves the
specification and investigation of new formal systems such as logics or
programming languages. A very common stumbling block in this process is
formalising systems with variable binding (for example, first-order logic or the
lambda calculus), as the otherwise intuitive concepts of variable names, capture
and substitution are quite tricky to express formally, such as in a proof
assistant. There is extensive and ongoing research in this area, approaching the
problem from practical (e.g. libraries) or theoretical (e.g. an algebraic
description of variable binding) perspectives. Moreover, reasoning about formal
systems (often called metatheory) brings about further difficulties.
Metavariables often stand for arbitrary terms of the language, and their
substitution properties differ from the ones of object variables: for example,
variable capture is not usually a concern with metasubstitution. There are
several nuances and questions related to the formal interplay of normal
substitution and metasubstitution which can be encountered both in "traditional"
language research, and the more widespread use of proof assistants (which
heavily rely on metavariables). There is some recent work that attempts to
address these questions by developing various higher-level formal systems and
metavariable calculi that can express these differing notions of substitution.

The aim of this research is to investigate a recently discovered connection
between the abstract syntax of languages with metavariables, and an opetopic
approach to higher-dimensional algebra. As a metavariable calculus, we will
concentrate on contextual modal type theory (CMTT): a constructive
interpretation of modal logic with contextual necessity that can serve as a
syntactic theory of metavariables and explicit substitutions. CMTT will be used
to explore the parallels between the abstract syntax tree of languages with
parameterised metavariables, and the tree structure of opetopic cells, a
fundamental shape used to define weak n-categories.

We plan to explore the details of this formal connection and address some of the
discrepancies that arise from comparing the Cartesian, second-order world of
CMTT with the linear, higher-dimensional setting of opetopes. In addition to
contributing to the ongoing research of a comprehensive algebraic theory of
type systems and computational calculi, this development would benefit both
higher-dimensional algebra and type theory. Firstly, it would give a formal,
syntactic reasoning framework for higher-dimensional algebra, simplifying its
proof language and handling the coherence conditions which become difficult to
work with at higher dimensions. Secondly, it could provide new insight into
higher-dimensional type theory from the perspective of general higher
categories, rather than the more restricted class of higher-groupoids (which
form the basis of homotopy type theory).

Due to its interdisciplinary nature, this project can be expanded into several
directions. One line of research would be a deeper examination of the algebraic
structure of a near-semiring, which often arises both in mathematics and
computer science, including the proposed connection between metavariables and
opetopes. We can also explore other modal logics and type theories with similar
meta-theoretic properties, with provability logic being a promising candidate
due to its reflective features (reasoning about the provability of a statement
in some base logic) and connections to staged computation.