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

9875536 J. Gregory Morrisett 我们正在研究低级但安全的编程语言的设计、应用程序和基础。 其目标与 C 语言一样，为程序员（和编译器）提供对指令和内存管理进行严格控制的选项，但与 Java 或 SML 等高级语言一样，提供设计大型系统所需的抽象和安全机制。 特别是，我们正在探索支持消除不必要的动态测试、提供对数据布局的手动控制以及对内存对象的分配进行细粒度控制的类型系统，所有这些都不会牺牲高级语言的安全保证。 我们预计这些低级语言的类型系统将具有许多引人注目的优势。 首先，对自动生成的代码或自动内存管理器不满意的程序员将可以手动优化代码。 只要生成的代码继续进行类型检查，程序员就可以确信代码仍然是安全的。 其次，类型化低级语言可以充当编译器中间语言或目标语言。 在这里，这些类型可用于支持高级优化，以确保维护编译不变式，并支持可扩展系统中的安全性。 最后，类型化低级语言可以充当高级语言系统和低级服务（例如运行时系统、操作系统或硬件设备）之间的安全“粘合剂”，从而提供从遗留软件到下一代系统的演进路径。

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.