CAREER: Type-Driven Language Technology for Software and Information Infrastructure

CCR-9984812CAREER：用于软件和信息基础设施的类型驱动语言技术Karl Crary本研究试图通过从三个方面利用类型理论来解决开发、维护和部署现代软件系统所面临的挑战：编程语言设计、基于语言的安全机制和类型化编译。语言设计研究的重点是支持大规模编程，特别是模块系统，用于将软件项目分解为可管理的部分，以及能够指定和执行复杂程序不变量的类型系统。安全研究的重点是不可信移动代码的安全检查和认证系统。特别是，它调查了这些系统的扩展，既支持更严格的安全策略(包括资源使用的限制)，又放松了对不影响安全性的代码方面的限制。类型化编译研究旨在提高编译器的技术，这些编译器将类型信息从源代码保存和利用到可执行文件中；这是其他两个途径中每一个途径的使能技术，提供高级语言的高性能编译，并为生成的可执行文件提供安全认证。该教育项目还试图通过让本科生熟悉关于程序的结构和推理的基本正式技能，以及让研究生熟悉类型理论语言设计和编译，来应对同样的挑战。

CCR-9984812CAREER: Type-Driven Language Technology for Software andInformation InfrastructureKarl CraryThe research seeks to address challenges faced in developing, maintaining and deploying modern software systems by exploiting type theory along three avenues: programming language design, language-based security mechanisms, and typed compilation. The language design research focuses on support for large-scale programming, particularly module systems, for breaking up software projects into manageable pieces, and type systems capable of specifying and enforcing complex program invariants. The security research focuses on systems for checking and certifying the safety of untrusted mobile code. In particular, it investigates the extension of these systems both to support tighter security policies (including bounds on resource usage) and to loosen their restrictions on aspects of code not affecting safety. The typed compilation research seeks to advance the technology of compilers that preserve and exploit type information from source code to executables; this is the enabling technology for each of the other two avenues, providing high-performance compilation of advanced languages, and certification of the resulting executables for safety. The educational program also seeks to address these same challenges by familiarizing undergraduate students with basic formal skills for structuring and reasoning about programs, and graduate students with type-theoretic language design and compilation.