CPSC 539B, Compiler Theory

Term 2 (Spring) 2019

This is the course website for the 2019 Term 2 CPSC 539B Topics in Programming Languages: Compiler Theory.






Mon. Wed. Fri.




ICCS 246




William J. Bowman







Office Hours:


By appointment; check my calendar and email me.





Mon, Dec 31


Added initial draft of course calendar, homework 0.

Mon, Jan 7


Added reference book.

Tue, Jan 8


Updated course calendar, including HW1 dates and type systems dates.

Wed, Jan 9


Added homework 1.

Wed, Jan 9


Added announcement about office hours.

Wed, Jan 9


Added another reference book.

Mon, Jan 14


Updated calendar, references to book; started list of papers.

Mon, Jan 14


Extended hw1; added instructions for resolving ambiguities in homework.

Tue, Jan 15


Fixed a problem with is-zero? in hw1; is-zero? is not defined on booleans

Wed, Jan 16


Added lecture notes; added paper critique instructions

Wed, Jan 16


Added hw2

1  Come to Office Hours!

The first part of this course involves a crash-course in programming languages theory techniques, so we can get to reading compiler correctness papers. Students who lack theory or PL background find it going a fast. If you have a hard time keeping up, please email me. At the very least, we can schedule office hours. I may also slow down and cover some of the basics in more detail.


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:
  • Introduce students to reasoning about programs and program transformations.

  • Introduce students to space of compiler correctness.

  • Convince students to think about compilers in terms of judgments preserved.


For additional reading, I recommend the following freely available books

The vocabulary and notation will diverge somewhat from what I use in class. Grant et al.’s book may be somewhat easier to follow, but Harper’s book makes a lot of important details very precise.


It is well-known that the best laid plans often go awry. Therefore, this calendar subject to change.








Wed, Jan 2.




HW 0 Assigned


Fri, Jan 4.


Syntax and operational semantics


HW 0 Due


Harper Chp 4.1, 5.1,5.2; Grant et al. Chp 2, 3

Mon, Jan 7.


Syntax and semantics continued



Chapters 1,2,3; Grant et al. Chp 2, 3

Wed, Jan 9.


Syntax and semantics; Type systems


HW 1 Assign


Grant et al. Chp 4

Fri, Jan 11.


Type systems



Grant et al. Chp 6 (particularly 6.2)

Mon, Jan 14.


Type systems continued



Harper Chp 6, Chp 22

Wed, Jan 16.


Logical Relations


HW 1 Due, before class


Harper Chp 46.2

Mon, Jan 21.


Modeling compilers



Chapter 8

Fri, Feb 1.


Read and discuss paper 1



Lecture Notes

Thanks to Chris for taking notes in a format that I can quickly convert to HTML, lecture notes are available here.


Ambiguities in homeworks can be resolved by "whatever interpretation makes your happy", but please make a note of which interpretation you chose.

HW 0

Bookmark this website and visit it every Monday this semester. Tell me your favorite programming language and compiler. Submit this homework via email at the above email address.

HW 1

Due by email 1:59 pm (before class) on Wed, Jan 16, or by Fri, Jan 18 if you need some extra time. Please use the subject line "[CSPC 539B] HW1". Please submit either in plaintext or structure plaintext (org-mode, markdown) or as a PDF. The homework is described hw1.html.

HW 2

Due by email 1:59 pm (before class) on Wed, Jan 23. Please use the subject line "[CSPC 539B] HW2". Please submit either in plaintext or structure plaintext (org-mode, markdown) or as a PDF. The homework is described hw2.html.


Starting approximately Feb 1., we (you) will start presenting and discussing papers in class.

Sign up for a paper at: https://docs.google.com/spreadsheets/d/1LahxpGU7oUnYspRwIw_yLt8S33D0n5TrAw4UVHJuj4w/edit?usp=sharing

Everyone should sign up as the presenter and discussion lead for at least one paper.

Paper Critiques

For each paper, you should send me a short (1-2 paragraph) critique. Start by briefly summarizing the paper, then describing its strengths and weaknesses. These are due before the first class in which we discuss the paper.

Please use the subject line "[CSPC 539B] paper title".


I’m planning for each paper to take up 2-3 days to present and discuss. One person will lead the presentation of the paper, and one person will lead discussion.

The presentation should be on the whiteboard, and you should not worry about polish. Part of the goal for this is to help you get confortable just talking about technical material without much prep (a skill you will need as a researcher). You may not understand everything in the paper, and that’s fine. The goal is to explain what you do understand, and discuss the paper to improve understanding.

The person leading discussion should ensure everyone is following the presented material, ask and encourage others to ask questions, and try to question implicit assumptions in the technical work.