Compiler Theory
Course Overview
Course Schedule
| Weeks | Topics |
|---|---|
| 1-5 | Basics of programming language theory (with homework) |
| 5-6 | Mathematical models of compilers (using a high-level language such as a functional or object-oriented language) |
| 6-12 | Seminars on compiler correctness (paper reading) |
| 12-15 | Class projects |
Course Project
The deliverable for the course project is a 5-page report consisting of mostly math and an in-class presentation. The goal of the project is to design a translation both satisfying a correctness property and violating another.
- Mathematically model the source and target language
- Describe the transformation
- State the first correctness property
- Argue that it holds for the transformation
- State the second correctness property
- Show a counterexample program
Expectation
Come to class with prepared questions and finished homework.
Overview
Compilers are traditionally thought of as transformations from programs in a source language to programs in a target language.
transform
Source programs ———————————> target programsHowever, this course encourages us to think about compilers as transformations on languages.
transform
Source language ———————————> target languageThe transformations should preserve desirable properties. In other words, for all programs in the source language, the compiler produces programs in the target language, preserving desirable properties. When we talk about correctness of compilers, we are talking about this property preservation characteristic of compilers. Some examples of desirable properties are security (e.g. not leaking passwords) and data encapsulation properties (e.g. not exposing internal methods).
This course focuses on four correctness properties.
Type preservation
Whole program correctness (traditionally called correctness, this property does not deal with external code linking)
Separate compilation (correctness while linking with other code)
e —> L ↓ ↓ e’ —> L where e is a program in the source language, e’ is a corresponding program in the target language, L is a library, L’ is a corresponding compiled library in the target language, —> represents linking (e is linked with L and e’ is linked with L’), and ↓ represents compilation.
Secure compilation (traditionally called full abstraction, this is a very abstract property, can represent any interesting property like not leaking passwords, interacting correctly with the outside world, etc.)
This course deals with correctness proofs of programs and program transformations.