ITR: Imperative Programming with Dependent Types

提案编号：ITR-0081316 PI：Xi，Hongwei机构：西校区，麻省理工学院标题：依赖类型的命令式编程编程是出了名的容易出错。因此，大量的方法已经被开发出来，以促进程序错误检测。 拟议的研究旨在丰富实际的命令式编程与类型的纪律，允许规范和推理显着更精确的信息程序比那些强制执行的语言，如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.