Typed Compilation

Typed Compilation (15-819B) is a graduate-level course on advanced compilation strategies that preserve and exploit type information. The course's topics include type checking, type-preserving program transformations, type-directed optimization, type systems for low-level languages, and certifying compilation.

Time and place

The course meets Mondays and Wednesdays in Wean Hall 5409B.

Textbook

The textbook for the course is Type Systems by Benjamin Pierce. The book is available on-line.

Topics

The topics to be covered (if time permits) are as follows. Many of these topics relate directly to research papers, which are given as supplementary reading.

Introduction
- Preliminaries
- Subtyping elimination (supplementary reading)
Data representation
- Type-directed unboxing (supplementary reading)
- Intensional type analysis (supplementary reading)
- "Optimal" unboxing (supplementary reading)
Module compilation
- Phase splitting
- Translucent sums and singleton kinds (supplementary reading: 1, 2, 3)
Core compilation
- Continuation-passing style translation (supplementary reading)
- Monomorphic closure conversion (supplementary reading)
- Polymorphic closure conversion (supplementary reading)
- Correctness proofs (using simulation and logical relations)
Intensional type analysis revisited
- Explicit type representations (supplementary reading)
- Inductive kind systems (supplementary reading)
Typechecking intermediate languages
- Decidability proofs using strong normalization (supplementary reading)
- Foundations for type checking (supplementary reading)
- Decidability proofs using logical relations (supplementary reading)
Low-level type systems
- Abstract models of memory (supplementary reading)
- Typed assembly language (supplementary reading)
- Stack types (supplementary reading)
- Proof-carrying code
Memory management
- Tag-free garbage collection
- Region inference
- Capability type systems
Dependent types
- Array bounds check elimination
- Resource bound certification
- Synthetic dependent types