The Fox Project
Typed Intermediate Languages

Contents Recent Talks | Recent Publications | Software | Collaborations | Further Links
Elsewhere Bibliography

Typed intermediate languages extend the benefits of type safety enjoyed by high-level source programming languages to the intermediate and target languages of a compiler. This is achieved by a generalization of syntax-directed compilation, called type-directed compilation. In a type-directed compiler, source code is translated into object code, and, at the same time, the type of the source code is translated into a type of the object code. The translation of the source code is guaranteed to have as its type the translation of the source type, so that well-typed programs at the source level are translated into well-typed programs at the object level.

Since well-typed source programs enjoy strong safety properties, so also do the corresponding target programs. By type checking the target code we can assure ourselves of its safety without having to trust the correctness of the compiler. A compiler that generates typed object code is an example of a certifying compiler whose object code can be mechanically checked for safety by any user of its generated code. Certifying compilers therefore provide a foundation for trust-free code dissemination in which code can be shared in an untrusted environment without sacrificing safety. By type checking intermediate code during compilation, we may build a self-checking compiler that verifies its own integrity by type checking the intermediate code produced by each compiler transformation. This greatly enhances the reliability of the compiler and greatly facilitates team development.

Type-directed certifying compilers support heterogenous component integration. Since typed object code comes equipped with types, we may rely on its safety without assuming that it arises from any one compiler or any one language. The same typed object code may arise from several different compilers for several different (type-safe) languages. This type information may then be used to mediate component integration to ensure the safety of composite systems. A type-safe linker can ensure that the typing requirements of individual components are satisfied when they are linked, either statically or dynamically, in a running system.

Type-directed compilers support the generation of efficient object code. Most existing compilers make serious compromises of efficiency in order to support automatic storage management or to permit the decomposition of programs into independent modules or components. By exploiting type information during compilation and at execution time, a type-directed compiler can avoid these compromises while preserving the benefits of storage management and modularity.

The Fox Project pioneered the development of type-directed compilers. The project is currently investigating both the foundations of type-directed compilation, such as the design of type systems for intermediate and object code, and the engineering problems of implementing type-directed compilers for full-scale programming languages. Our current research artifact is the TILT compiler (Typed Intermediate Languages, Two) for Standard ML.

Overview references:

Recent Talks

The Practice of Type Theory in Programming Languages.
Robert Harper.
Dagstuhl 10th Anniversary Symposium, Saarbruecken, Germany, August, 2000.
Typed Assembly Language: Type Theory for Machine Code.
Karl Crary.
PCC Workshop.
Santa Barbara, California, June 2000.

Recent Publications

A Type System for Higher-Order Modules.
Karl Crary, Robert Harper, and Derek Dreyer.
Submitted for publication to Twenty-Ninth Symposium on Principles of Programming Languages (POPL'02).
Toward a Practical Type Theory for Recursive Modules.
Derek R. Dreyer, Robert Harper, and Karl Crary.
Technical Report CMU-CS-01-112, March, 2001.
Automated Techniques for Provably Safe Mobile Code.
Christopher Colby, Karl Crary, Robert Harper, Peter Lee, and Frank Pfenning.
To appear, Theoretical Computer Science, 2001.
Implementing the TILT Internal Language.
Leaf Petersen, Perry Cheng, Robert Harper, and Chris Stone.
Technical Report CMU-CS-00-180, December, 2000.
A Language-Based Approach to Security.
Fred B. Scneider, Greg Morrisett, and Robert Harper.
Informatics: 10 Years Ahread, 10 Years Back. Conference on the Occasion of Dagstuhl's 10th Anniversary. Springer-Verlag Lecture Notes in Computer Science v. 2000.
Sound and Complete Elimination of Singleton Kinds.
Karl Crary.
2000 Workshop on Types in Compilation.
Typed Compilation of Inclusive Subtyping.
Karl Crary.
2000 International Conference on Functional Programming.
Type Equivalence in a Language with Singleton Kinds.
Christopher Stone and Robert Harper.
ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages. January, 2000.


Our work on type-directed compilation is based on the TILT Compiler for Standard ML.
  • The TIL Compiler is a type-directed compiler for the Standard ML core language. The source code is available, but this version of the compiler is no longer maintained.
  • The TILT Compiler for Standard ML is under active development. The current version is available for download under an open source license.


Related Links

  • The FLINT Project at Yale University is developing a universal typed intermediate format language for Java, Standard ML, and C.
  • The Proof Carrying Code Project at Princeton University is developing a foundational approach to proof-carrying code based on an operational interpretation of object code type systems.
  • The Church Project at Boston University is investigating sophisticated type systems for intermediate languages to support efficient compilation of higher-order languages.
  • The SML SourceForge Site is the repository for all Standard ML compilers and related code.

[ Home | Contact Information | Publications | Researchers ]
[ FoxNet | Typed Intermediate Languages | Proof-Carrying Code ]
[ Logical Frameworks | Staged Computation | Language Design ]