CAREER: Design, Applications, and Foundations of Safe, Low-Level Programming Languages

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

9875536 J. Gregory MorrisettWe are examining the design, applications, and foundations of low-level, but safe programming languages. The goal is as in C, to give programmers (and compilers) the option of tight control over instructions and memory management, but as with high-level languages such as Java or SML, provide the abstraction and safety mechanisms needed to engineer large systems. In particular, we are exploring type systems that support the elimination of unnecessary dynamic tests, provide manual control over data layout, and give fine-grained control over the [de]allocation of memory objects, all without sacrificing the safety guarantees of high-level languages. We expect that the type systems for these low-level languages will have a number of compelling benefits. First, a programmer unsatisfied with automatically generated code or automatic memory managers will have the facilities to hand-optimize the code. As long as the resulting code continues to type-check, the programmer can be assured that the code is still safe. Second, typed low-level languages can serve as compiler intermediate or target languages. Here, the types can be used to support advanced optimizations, to ensure that compilation invariants are maintained, and to support security in extensible systems. Finally, typed low-level languages can serve as safe "glue" between high-level language systems and low-level services, such as runtime systems, operating systems, or hardware devices, thereby providing an evolutionary path from legacy software to next-generation systems.