On this page:
CPSC 539B – Compiler Theory

CPSC 539B – Compiler Theory

Compilers are responsible for writing almost all of the programs that get executed. Like all programs, compilers have bugs. But unlike most programs, when compilers have bugs, they can insert bugs into other peoples’ code and give programmers little recourse.

All compilers have bugs, and this course will teach you what a compiler bug is, how to reason about compilers so you better understand where the bugs are and how to prevent bugs if you ever write a compiler. This course will introduce some techniques of formal reasoning about programs, programming languages, and compilers. The course will then review recent compiler correctness research, and study the different ways a compiler can be correct, or incorrect, and how to implement a correct compiler and prove that it’s correct.

My goals with this course are:

    1 Announcements and Changes

      1.1 Announcements

      1.2 Changes

    2 Syllabus, CPSC 539B

      2.1 Land Acknowledgement

      2.2 Course Description

      2.3 Course Information

      2.4 Prequisites

      2.5 Course Materials

      2.6 Contacts

      2.7 Course Structure

        2.7.1 Structure for Introduction

        2.7.2 Structure for Seminar



      2.8 Grading

      2.9 Learning Objectives

      2.10 Schedule of Topics

    3 Course Calendar

    4 Lecture 1 – Introduction to Rebuilding the Universe

      4.1 What is math?

      4.2 The Two Axioms

        4.2.1 The First Axiom: Implication

        4.2.2 The Second Axiom: Induction

        4.2.3 Defining Not-False Things: Rules of Thumb

      4.3 Defining a Language

        4.3.1 Modeling a Collection of Expressions

    5 Lecture 2 – Modeling a Language, Continued

      5.1 A little review

      5.2 Making Formal Judgments Really Formal

      5.3 BNF Grammars – A short-hand for simple judgments

      5.4 Modeling Operatings on Expressions

      5.5 Modeling Evaluation

    6 Lecture 3 – The First Complete Model of a Language

      6.1 To a Model of an Interpreter

      6.2 Modeling Functions, and a useful pattern for adding new features

        6.2.1 Capture-Avoiding Substitution

      6.3 Computing with Judgments

    7 Homework 1 – Practice Modeling a Language

      7.1 Part 1: Define a collection of expressions

      7.2 Part 2: Define operations on expressions

      7.3 Part 3: Properties

      7.4 Part 4: Prove some stuff

        7.4.1 About dictionaries

        7.4.2 About numbers

    8 Lecture 4 – Type Systems

      8.1 Properties of Programs

      8.2 The Language of NatBool Expressions

      8.3 A Type System for NatBool

      8.4 A Type System for λNatBool

      8.5 Type Systems and Type Annotations

    9 Homework 2 – Practice with Type Systems

      9.1 Type Systems

      9.2 Proof by Induction/Type Safety

    10 Lecture 5 and 6 – Proof by Induction

      10.1 Some Facts About Natural Numbers

      10.2 An inductive proof is a recursive function over derivations

    11 Lecture 10 – Introduction to Compiler Correctness

      11.1 Closure Conversion Review

      11.2 What even is compiler correctness

        11.2.1 Whole-Program Correctness

        11.2.2 Correctness of Separate Compilation

        11.2.3 Compilitional Compiler Correctness

      11.3 Proving Compiler Correctness