ITR: Imperative Programming with Dependent Types

点击翻译按钮获取中文摘要

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.