ITR: Imperative Programming with Dependent Types

提案号：ITR-0081316PI: Xi， hongwei机构：West Campus， University of cincinnati题目：命令式编程与依赖类型编程是出了名的容易出错。因此，已经开发了大量的方法来促进程序错误检测。拟议的研究旨在丰富实际命令式编程的类型规程，允许规范和推断比Java和标准ML等语言中强制执行的更精确的程序信息。开发这种类型规程的主要动机是使程序员能够使用类型捕获更多的程序属性，例如内存安全，然后通过类型检查强制这些捕获的属性。这种做法允许在更短的时间内检测更多的程序错误。另一个动机是使用类型规则为低级代码生成内存安全证明，从而有效地生成断言其自身内存安全的携带证明的代码。简而言之，该研究研究了实用命令式编程在高层和低层的类型学科，旨在生产不仅运行更健壮，而且维护成本更低的软件。

Proposal Number: ITR-0081316PI: Xi, HongweiInstitution: West Campus, University of CincinnatiTITLE: Imperative Programming with Dependent TypesProgramming is notoriously error-prone. As a consequence, a greatnumber of approaches have been developed to facilitate program errordetection. The proposed research intends to enrich practical imperativeprogramming with a type discipline that allows for specification andinference of significantly more precise information on programs thanthose enforced in languages such as Java and Standard ML. The primarymotivation for developing such a type discipline is to enable theprogrammer to capture with types more program properties such asmemory safety and then enforce these captured properties throughtype-checking. This practice allows for detecting more program errorsin less time. Another motivation is to use the type discipline togenerate memory safety proofs for low-level code and thus effectivelyproduce proof-carrying code that asserts its own memory safety. Inshort, the research studies a type discipline for practical imperativeprogramming at both high and low levels, aiming for producing softwarethat is not only more robust to run but also less costly to maintain.