Dependent Typing for Imperative Programs

命令式程序的依赖类型

• 批准号: 2880924
• 金额: --
• 依托单位: University of St Andrews
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2023
• 资助国家: 英国
• 起止时间: 2023 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2880924
• 关键词: Dependent; Typing; Imperative; Programs

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.

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