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

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

CCR-9984812 CAREER: Type-Driven Language Technology for Software and Information Infrastructure Karl Crary The 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.