Prof. Stephen Chong
with Aaron Bembenek, Anitha Gollamudi, David Holland, and others
Spring 2020

Course information

The topic of CS252 changes each semester. This semester (Spring 2020) we will collectively and collaboratively learn about verified and secure compilation. The class is intended to teach both about the theory and the practice of constructing verified compilers. While we will be reading a number of papers about verified and secure compilation, a signficant part of the learning in the class will be through constructing (individually and/or collectively) a verified compiler.

The course will be a combination of paper discussions, labs (where we collectively work on code), and maybe code/proof walkthroughs. We will be figuring this out as we go. See the lecture schedule for the current plan.

For those taking the course for credit, evaluation will be based on class participation, and a final project. Auditors are welcome, but must participate in discussion and devote time outside of the class to working on the project(s). There will be some coding assignments; while these will not be graded, they will be discussed, so it is expected that class participants will complete them.

Recommended Prerequisites

The course is intended for graduate students at all levels as well as advanced undergraduates. It is expected that students have taken a course in the foundations of programming languages, such as CS 152 and have taken a course in compilers, such as CS 153.

Some familarity with Coq is required. If you are not currently comfortable using Coq, some of your time in the first few weeks will need to be spent getting up to speed on Coq, by going through selected parts of either Volumes 1 and 2 of Software Foundations or Formal Reasoning about Programs by Adam Chlipala.


Piazza will be the primary medium for out-of-class communication. Sign up for Piazza here.

Time and Place

Tuesdays and Thursdays, 10:30am-11:45am, room MD 323.

Schedule and Reading List

The Zoom meeting room is [removed]. See this page for more info about our remote classroom meetings.

This embedded spreadsheet has the schedule for the course, as well as a list of papers that we might read (see the "Reading List" tab).

Diversity and Inclusion

I would like to create a learning environment that supports a diversity of thoughts, perspectives and experiences, and honors your identities (including race, gender, class, sexuality, religion, ability, etc.) To help accomplish this:

If you ever are struggling and just need someone to talk to, feel free to stop by office hours, or to reach out to me and we can arrange a private meeting.

Inclusive Learning and Accessibility

Your success in this class is important to me. We will all need accommodations because we all learn differently. If there are aspects of this course that prevent you from learning or exclude you, please let me know as soon as possible. Together we'll develop strategies to meet both your needs and the requirements of the course.

I encourage you to visit the Accessible Education Office to determine how you could improve your learning as well. If you need official accommodations, you have a right to have these met. There are also a range of resources on campus. The Bureau of Study Counsel provides many resources, including academic counseling and peer tutors.

Mental Health

If you experience significant stress or worry, changes in mood, or problems eating or sleeping this semester, whether because of CS252 or other courses or factors, please do not hesitate to reach out immediately, at any hour, to any of the course staff to discuss. Everyone can benefit from support during challenging times. Not only are we happy to listen and make accommodations with deadlines as needed, we can also refer you to additional support structures on campus, including, but not limited to:

Financial Aid

We do not require that students purchase any books, hardware, or software. While not required, having one's own laptop is helpful. Students without their own laptops are encouraged to reach out at the start of the course to discuss possibilities.

Collaboration Policy

Discussion and the exchange of ideas are essential to doing academic work. For paper readings, assignments, in-class exercises, etc., you are encouraged to consult with your classmates, and to share sources. For the class project, you may work in groups, and work submitted for evaluation may be the result of the collaborative effort of your group. All members of the group should be clearly indicated to the course staff, and the course staff should be notified if group membership changes. The class project should be original research, and the same standards of professional conduct for publishable research apply to your class project.

When submitting the final project, College students will include a statement affirming the Harvard College Honor Code: "I affirm my awareness of the standards of the Harvard College Honor Code."

College students: Please see the Honor Code.