Modal type theory and Higher-dimensional algebra

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

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.