The TILT Compiler Project

The TILT (or TIL-Two) Compiler Project is a joint effort between researchers at Cornell and Carnegie Mellon. The goal of the project is to produce a compiler for the ML-family of programming languages (SML'97, Caml Special Light, and KML) that takes advantage of types throughout compilation in order to produce better code without compromising safety or correctness.

The guiding principle behind TILT is to always manipulate Typed Intermediate Languages (hence the name). Consequently, at any stage during compilation, we can automatically type-check the code to ensure that a wide class of important safety properties have been maintained by the compiler. The ability to automatically type-check the intermediate code gives us the leverage to...

• ...detect and isolate bugs in the compiler. This is important when working on a large compiler project where a variety of people are building components that must snap together. The more compiler invariants that we can encode in the types of the intermediate terms, the more unlikely it is that someone working on the compiler can introduce a subtle, hard-to-find bug.
• ...take advantage of types to produce smaller, faster code. As with the TIL-1 prototype compiler, TILT takes advantage of types at compile, link, and run-time in order to support unboxed, tag-free data structures, efficient calling conventions, and efficient automatic memory management.
• ...send low-level, heavily optimized code over the network to untrusting hosts. Not only does this reduce the latency of just-in-time (JIT) compilation, but it also reduces the need for the host to trust the majority of the compiler. Instead, the creator of a network agent may compile to very low-level code and the host need only to type-check the code and then perform the last few stages of compilation.
• ...construct proofs of compiler correctness. Various compiler stages, such as the unboxing phase, the closure conversion phases, and the garbage collector have all been modelled and proven correct in a suitable sense. These proofs greatly benefited from (and in fact required) the type structure present in the intermediate langauges.

Papers Related to TILT

• A Type Theoretic Account of Standard ML 1996 (Version 2), Robert Harper and Chris Stone, CMU Technical Report CMU-CS-96-136R. Also appears as Fox Memorandum CMU-CS-FOX-96-02R.
• Semantics of Memory Management for Polymorphic Languages, Greg Morrisett and Robert Harper, CMU Technical Report CMU-CS-96-176 [Also appears as CMU-CS-FOX-96-04], September, 1996.
• Compiling with Types, Greg Morrisett, (gzipped postscript), Ph.D. Thesis, Published as CMU Technical Report CMU-CS-95-226, December, 1995.
• TIL: A Type-Directed Optimizing Compiler for ML, D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, P. Lee, 1996 SIGPLAN Conference on Programming Language Design and Implementation.
• The TIL/ML Compiler: Performance and Safety Through Types, G. Morrisett, D. Tarditi, P. Cheng, C. Stone, R. Harper, P. Lee, 1996 Workshop on Compiler Support for Systems Software.
• Typed Closure Conversion , Yasuhiko Minamide, Greg Morrisett, and Robert Harper , To appear in the 1996 Symposium on Principles of Programming Languages. Extended version published as CMU Technical Report CMU-CS-FOX-95-05 , July 1995.
• Compiling Polymorphism Using Intensional Type Analysis, Robert Harper and Greg Morrisett Proc. of the 22nd Annual ACM Symposium on Principles of Programming Languages, San Francisco, January 1995.

People Involved with TILT:

Some Related Projects:

• Dexter Kozen's Security Project
• The Fox Project
• Flint & SML/NJ
• The Church Project
• The ML-Kit with Regions Project

Source Code:

• The sources for the original TIL compiler are available for perusal. As we're no longer actively developing this version of the compiler, we can't really offer any help in setting up or configuring it to run.