KARL CRARY
Assistant Professor, Computer Science
www

My research interests are in the design and implementation of advanced programming languages and in applying programming language technology to improve the development, maintenance, and performance of software systems. I am particularly interested in the application of types to the structure and implementation of programming languages.

A current focus of my research is on typed compilation. Compilation using types offers some compelling benefits over conventional, untyped compilation. For example, preserving types through compilation provides additional information that may be used to optimize programs. Type-based optimizations are particularly useful for compiling advanced programming languages, such as ML. Advanced programming languages provide many features such as first-class functions, automatic memory management, polymorphism and abstraction, that are valuable to programmers but are also hard to implement efficiently. Modern implementation strategies, including type-based optimization, allow advanced languages to be implemented roughly as efficiently as less advanced ones. For instance, the TIL (Typed Intermediate Languages) compiler for ML, one project I work on, uses type-based optimizations to obtain a 3-fold speedup over other ML compilers.

An even more important benefit of typed compilation lies in its application to mobile code security. With the increasing importance of the widely distributed computing (particularly with the World Wide Web), it has become impractical for agents to limit their computing interactions to other agents whom they trust. This leads directly to a need for mechanisms whereby an agent can safely execute untrusted and potentially malicious programs. However, it is important that such mechanisms not substantially sacrifice performance, as is the case with run-time checking mechanisms. Typed compilation gives us a tool for producing certified executables, which can be statically determined to be safe before execution. This certification strategy works by attaching types to mobile code; that code is then type-checked and is run only if type-checking succeeds. If it does succeed, the formal semantics of the type system guarantees that code is safe.

For this to work requires a type system suitable for low-level code, in particular for machine binaries. However, most research into type systems has focused on high-level languages, in part because low-level languages can be uncooperative to type-theoretic analysis. Recently, I and others have been studying typed assembly languages, machine-level programming languages with sound type systems. In a typed assembly language, one can program with direct access to machine resources without sacrificing the safety guarantees provided by typed high-level languages. In practice, however, typed assembly code is typically produces by a typed compiler from high-level source code. My ongoing research into typed assembly languages focuses on enhancing their type systems both to make them more flexible and to strengthen the safety properties they can guarantee.