Dependent Typing for 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.