Modal type theory and Higher-dimensional algebra

对编程语言和类型理论的研究通常涉及对新的形式系统的描述和研究，例如逻辑或编程语言。这个过程中一个非常常见的绊脚石是使用变量绑定来形式化系统(例如，一阶逻辑或lambda演算)，因为变量名、捕获和替换等其他直观的概念很难正式表达，例如在证明助手中。在这一领域有广泛且正在进行的研究，从实践(例如，库)或理论(例如，变量绑定的代数描述)的角度来处理该问题。此外，关于形式系统的推理(通常称为元理论)带来了更多的困难。元变量通常代表语言的任意术语，它们的替代属性不同于对象变量：例如，变量捕获通常不是元替代的问题。有几个细微的差异和问题与正常替代和元替代的形式相互作用有关，这在“传统的”语言研究中都可以遇到，也可以在更广泛地使用证明助手(严重依赖元变量)中遇到。最近有一些工作试图通过开发各种更高级别的形式系统和元变量演算来解决这些问题，这些系统和元变量演算可以表达这些不同的替换概念。本研究的目的是调查最近发现的具有元变量的语言的抽象语法与高维代数的开放方法之间的联系。作为一种元变量演算，我们将集中讨论语境情态类型理论：一种具有语境必然性的对情态逻辑的建构性解释，可以作为元变量和显式替换的句法理论。Cmtt将被用来探索带有参数化元变量的语言的抽象语法树与用于定义弱n范畴的基本形状--视点细胞的树结构之间的相似之处。我们计划探索这种形式联系的细节，并解决由于比较Cmtt的笛卡尔、二阶世界与线性的、高维的opetope设置而产生的一些差异。除了有助于正在进行的关于类型系统和计算演算的全面代数理论的研究之外，这一发展还将使高维代数和类型理论都受益。首先，它将为高维代数提供一个形式化的句法推理框架，简化其证明语言，并处理在高维代数上变得难以处理的一致性条件。其次，它可以从一般更高范畴的角度对高维类型理论提供新的见解，而不是更受限制的更高群胚的类别(构成同伦类型理论的基础)。由于其跨学科的性质，该项目可以扩展到几个方向。一条研究路线是对近半环的代数结构进行更深入的研究，这通常出现在数学和计算机科学中，包括提出的元变量和opetope之间的联系。我们还可以探索其他具有类似元理论性质的模态逻辑和类型理论，可证性逻辑是一个很有前途的候选者，因为它的反射特征(关于某个基本逻辑中语句的可证性的推理)以及与阶段性计算的联系。

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 tocontributing 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.