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
(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
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
Papers Related to TILT
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
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],
- Compiling with Types, Greg
Morrisett, (gzipped postscript), Ph.D. Thesis,
Published as CMU Technical Report CMU-CS-95-226,
- 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
- 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
- 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
- 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,
People Involved with TILT:
Some Related Projects:
- 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.
This page maintained by firstname.lastname@example.org, last updated on
17 June 1997