KnowledgeBase » SEMINAR » ID = 469

Type Methodology for Modern Languages and Compilers

by Karl Crary
1997-1998

Modern programming languages balance two needs: the need to provide correct and efficient compilers, and the need to specify complete and rigorous semantics. Unfortunately, it has typically been the case that languages with good rigorous semantics (such as ML) have been challenging to implement efficiently, and that languages that are more easy to implement (such as Java)have been semantically flawed.

However, these goals need not be in opposition. In this talk, I show how methods based in type theory can lead to both better compilers and better semantics for modern programming languages. I discuss how type theory may be used as a framework for defining semantics. Such a framework provides benefits for proving valuable properties about programs and languages, while remaining computational and useful to language implementers. One dividend of this view relates to typed compilation. Compilers may also use type information to produce more efficient and secure code, but existing compilers have not been able to take full advantage of type information because we have not known the right typing mechanisms for low-level code. I present typed assembly language, the first set of typing mechanisms applicable to native code.

Some of the results presented here were developed in collaboration with Greg Morrisett, David Walker and Neal Glew.)