Colloquium Details
TILT: Compiling With Types For Optimization and Certification
| Author: | Leaf Petersen Carnegie Mellon University |
|---|---|
| Date: | April 15, 2003 |
| Time: | 15:30 |
| Location: | 220 Deschutes |
Note: Special Day
Abstract
Types serve as a means for specifying invariants of programs in an automatically checkable way. Traditional compilers check that these invariants hold, but subsequently discard most type information. The TILT compiler preserves type information deep into the compilation process and takes advantage of these invariants to produce more efficient code.
Recent work has been aimed at extending TILT to push types all the way to object code, allowing the native object code to be checked for safety. Pushing types to this lowest level presents significant challenges for designers of compiler internal languages. In this talk, I give an overview of typed compilation as it is currently done in TILT, and discuss the low-level type theories needed to compile to typed object code. As a detailed example, I explore a type theory with close connections to ordered logic that makes explicit some of the low-level data layout and memory allocation issues. Important invariants of the allocation model are captured naturally in the types, permitting fine-grained optimization of data allocation and initialization.
Biography
Leaf is a prospective Ph.D. candidate from the School of Computer Science of Carnegie Mellon University (Summer 2003). He received his B.A. from Williams College, Summa Cum Laude. His research interests include type theory, advanced programming languages - theory, design, and efficient implementation, compiling with types, object-oriented languages, module systems and data representation languages.