ITR: Imperative Programming with Dependent Types

University Of Cincinnati Main Campus, Cincinnati OH

Investigators

Abstract

Proposal Number: ITR-0081316 PI: Xi, Hongwei Institution: West Campus, University of Cincinnati TITLE: Imperative Programming with Dependent Types Programming is notoriously error-prone. As a consequence, a great number of approaches have been developed to facilitate program error detection. The proposed research intends to enrich practical imperative programming with a type discipline that allows for specification and inference of significantly more precise information on programs than those enforced in languages such as Java and Standard ML. The primary motivation for developing such a type discipline is to enable the programmer to capture with types more program properties such as memory safety and then enforce these captured properties through type-checking. This practice allows for detecting more program errors in less time. Another motivation is to use the type discipline to generate memory safety proofs for low-level code and thus effectively produce proof-carrying code that asserts its own memory safety. In short, the research studies a type discipline for practical imperative programming at both high and low levels, aiming for producing software that is not only more robust to run but also less costly to maintain.