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.
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 have a name and/or set of pronouns that differ from those that appear in your official Harvard records, please let me know!
- If you feel like your performance in the class is being impacted by your experiences outside of class, please don't hesitate to come and talk with me. I want to be a resource for you. If you prefer to speak with someone outside of the course, members of the SEAS Committee on Diversity, Inclusion, and Belonging are excellent resources.
- I (like many people) am still in the process of learning about diverse perspectives and identities. If something was said (by anyone) in class, office hours, Piazza, or project group work that made you feel uncomfortable, please talk to me about it.
- As a participant in course discussions, office hours, and group projects, you should also strive to honor the diversity of your classmates.
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.
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:
- Counseling and Mental Health Services, 617-495-2042 or 617-495-5711 after hours
- Let's Talk
- Room 13, 617-495-4969
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.
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.