Dependent Typing for Imperative Programs

这个项目旨在研究依赖类型系统对命令式编程语言的适用性。依赖类型的编程语言允许在类型级别进行计算，允许类型在值之间变化，因此能够在类型级别上以任意精确的程度表达问题的约束（直到可能只有一种正确的方法来编写程序）。这个思想已经被用于创建定理证明语言，如Coq和Agda，在这些语言中，由于依赖类型系统和高阶谓词逻辑之间的Curry-Howard同构，人们可以使用MLTT（标准依赖类型系统）证明逻辑语句。在更通用的函数领域中的其他语言也在其系统中集成了依赖类型，例如Idris。本博士的目的是研究这个概念在完全应用于命令式语言时的适用性，在命令式语言中，变量可以被修改，并且有可变内存的一流概念。当与依赖类型配对时，这通常会造成困难，因为它使类型检查不可确定。然而，存在以代数方式表示不同类型副作用的形式化方法，因此类型检查变得可确定，或者至少是可控制的不可确定（标记区域）。线性逻辑（以及CH-iso的线性类型系统）、代数效应和线性时间逻辑都是可用于模拟各种杂质/对象寿命等概念的子结构系统，这些都是将被研究并应用于命令式语言的一部分。

This project aims to investigate the applicability of dependent type systems to imperative programming languages. Dependently typed programming languages allow computation at the type-level, by allowing types to range over values, and as a result being able to express the constraints of a problem to an arbitrarily precise degree on the type-level (to the point where there could be only one correct way to write the program). This idea has been used to create theorem proving languages such as Coq and Agda, where one can prove logic statements using MLTT (the standard dependent typing system) because of the Curry-Howard isomorphism between dependent type systems and higher-order predicate logic. Other languages in the more general-purpose functional domain have also integrated dependent types in their systems, such as Idris. The purpose of this PhD is to investigate the applicability of this concept when fully applied to imperative languages, where variables can be modified and there is a first-class notion of mutable memory. This poses a difficulty in general, when paired with dependent typing, because it renders type-checking undecidable. However, there exist formalised ways to represent different kinds of side-effects in an algebraic manner, so that type checking becomes decidable, or at least controllably undecidable (marked regions). Linear logic (and linear type systems by the CH-iso), algebraic effects, and linear temporal logic are all sub-structural systems that can be used to model various concepts of impurity/lifetime of objects/etc, and these are part of what will be investigated and applied to an imperative language.