Computer Science

Colloquium Details

Type Theory and the TILT Compiler

Abstract

With the growing presence of networked computers and mobile code, issues of program safety and security become increasingly important. A key tool is the use of typed programming languages such as Java or Standard ML, where the language itself guarantees that all valid programs satisfy certain safety properties.

Although this method depends on certainty that the source language actually is safe, there has been no proof for a real-life language. Languages in practice tend to be complex, irregular, and/or ill-defined. And even if such a proof were given for the source language, safety can be compromised by a malicious or buggy compiler.

In this talk I will discuss the use of typed intermediate languages as a tool both for the theory and the implementation of the Standard ML language. By showing how to translate ML programs into a theoretically tractable typed form, we can derive properties of ML itself. And by having the compiler use a strongly-typed intermediate representation for programs, we can preserve information necessary for certifying that the compiler's output preserves the safety properties of the input program. I conclude with an extended example showing how implementation choices in our TILT compiler for ML can drive intermediate language design and type-theoretic studies.

Biography