## Leaf Petersen

### Implementing the Internal Language of the TILT Compiler

The TIL compiler pioneered the idea of using typed intermediate
languages for compilation. Instead of using standard syntax directed
transformations, compilation in TIL proceeds via a series of type
directed transformations mapping well-typed terms to well-typed terms.
The compiler can use the type information and the invariants imposed
by the type system to assist with optimization and verification. The
TIL-Two (TILT) compiler extended this work to the full Standard ML '98
language including the module system. This extension required the
use of significantly more powerful and complex intermediate languages.

This talk will focus on one of the intermediate languages used in
TILT, called the MIL (Middle Intermediate Language). The MIL is a
predicative lambda calculus with dependent kinds that serves as the
main intermediate form for TILT. The MIL was designed to address both
the theoretical requirements for serving as the target of the
translation from SML '98 and the practical requirements imposed by the
implementation. In this talk, I will first present a restricted
mini-MIL calculus which contains the core constructs of the MIL. This
restricted calculus is powerful enough to express the structural
sharing of the module language, but suffers from some practical
problems - most notably the inability to express some types compactly.
To address this, I will present an extended mini-MIL calculus that
solves the compactness problem of the restricted calculus by allowing
undecorated singleton types at higher kinds - essentially introducing
an element of type inference into type-checking. The extended
calculus is related to the restricted calculus via a transformation
that eliminates the undecorated singletons.

May 12, 2000

3:30pm

Wean 8220