ITR: Imperative Programming with Dependent Types

提案编号：ITR-0081316PI：XI，宏伟机构：辛辛那提大学西校区TITLE：依赖类型命令式编程众所周知，编程容易出错。因此，已经开发了大量的方法来促进程序错误检测。拟议的研究旨在用类型规程来丰富实际的必需编程，该规程允许指定和推断关于程序的更精确的信息，而不是那些在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.