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.

Days

  

Time

  

Room

Mon. Wed. Fri.

  

15:00--16:00

  

ICCS 246

               

Instructor:

  

William J. Bowman

Office:

  

ICICS 389

Email:

  

wilbowma

Office Hours:

  

By appointment; check my calendar and email me.

Announcements

Date

               

Description

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.

Description

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.

References

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.

Calendar

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

Date

               

Subject

               

Homework

               

References

Wed, Jan 2.

               

Prelims

               

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.

Homework

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.

Papers

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".

Format

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.