1 Prerequisites and Description🔗

Prerequisite: a grade of C or better in CMSC330; and permission of instructor; or CMSC graduate student.

Credits: 3.

CMSC 838E is a graduate-level verified compilers course focused on developing machine-checked proofs of compiler correctness. The course studies how to specify the semantics of a high-level functional language, implement a compiler targeting a low-level assembly language, and prove that compilation preserves the meaning of programs.

The course assumes familiarity with a functional programming such as OCaml from CMSC 330, and, to a lesser extent, imperative programming in C and Assembly as covered in CMSC 216. Since the course builds significantly on CMSC 430, it is recommended undergraduate students have already completed 430 and that graduate students have taken a compilers course before, however in either case, highly motivated students should be able to keep up with the material without this background.

2 Course Workflow🔗

This course will be run as a collaborative research “workshop.” There will not be traditional lectures beyond the first few covering the background on functional programming and compilation. Once this background is covered, we will work collectively to accomplish goals we establish for our compiler. Students will work both in small teams and collectively with the whole class. Class time will be spent covering research papers relevant to our goals, discussing technical issues, and reviewing our collective work.

Outside of the scheduled class time, we will communicate primarily via Piazza.

Piazza is there for you to organize as a class, ask questions of each other, and get help from each other and the instructor.

3 Topics🔗

This course will be intentionally open-ended; we will collectively decide what to explore, but some potential topics include:

• Overview of compilation

• Operational semantics

• Mechanized semantics and proofs in Lean

• Interpreters

• Stack machines

• Compiler correctness

• Type systems, type soundness, type inference

• Variables and binding

• Functions, tuples, heaps, and pointers

• Lambda calculi

• Logical relations

• Unification and principal types

• Recursive types and step-indexed logical relations

• Language design

• Gradual types

4 Grading🔗

Grades are based on participation, assignments, and a final project:

• Participation: 20%

• Assignments: 20%

• Project: 60%

Participation means attending class, participating in discussions, and engaging with the course material. The project requires proposing, implementing, and writing up a small PL-related research project. Collaborative projects are encouraged.

5 Class meetings🔗

We will use the scheduled class times to meet synchronously in person.

6 Computing Resources🔗

Students are expected to use their own systems or resources provided by the department or university to develop the deliverables for this course.

Students may use whatever development tools are appropriate for their course work. Please make sure everything you build can be shared with the instructor.

7 Outside-of-class communication🔗

Asynchronous communication is done via Piazza. Please check Piazza at least once per weekday at a bare minimum.

8 Students with Disabilities🔗

Students with disabilities who have been certified by Disability Support Services as needing any type of special accommodations should see the instructor as soon as possible during the schedule adjustment period (the first two weeks of class). Please provide DSS’s letter of accommodation to the instructor at that time.

All arrangements for exam accommodations as a result of disability must be made and arranged with the instructor at least three business days prior to the exam date; later requests (including retroactive ones) will be refused.

9 University of Maryland Policies for Students🔗

Please read the university’s guide on Course Related Policies, which provides you with resources and information relevant to your participation in a UMD course.

Graduate students should also be familiar with the Graduate School’s Academic Policies.

10 Academic Integrity🔗

The Campus Senate has adopted a policy asking students to include the following statement on each examination or assignment in every course: "I pledge on my honor that I have not given or received any unauthorized assistance on this examination (or assignment)." Consequently, you will be requested to include this pledge on each exam and assignment. Please also carefully read the Office of Information Technology’s policy regarding acceptable use of computer accounts.

Projects may be completed collaboratively, therefore cooperation with others is not a violation of the University’s Code of Academic Integrity. However, your work must be your work. Plagiarism or the uncredited use of others’ work is not acceptable. Any evidence of this, or of unacceptable use of computer accounts, use of unauthorized materials, or other possible violations of the Honor Code, will be submitted to the Student Honor Council, which could result in an XF for the course, suspension, or expulsion.

If you have any question about a particular situation or source then consult with the instructor in advance.

It is the responsibility, under the honor policy, of anyone who suspects an incident of academic dishonesty has occurred to report it to their instructor, or directly to the Honor Council.

11 Course Evaluations🔗

If you have a suggestion for improving this class, don’t hesitate to tell the instructor. At the end of the semester, please don’t forget to provide your feedback using the campus-wide CourseEvalUM system. Your comments will help make this class better.

12 Right to Change Information🔗

Although every effort has been made to be complete and accurate, unforeseen circumstances arising during the semester could require the adjustment of any material given here. Consequently, given due notice to students, the instructors reserve the right to change any information on this syllabus or in other course materials. Such changes will be announced and prominently displayed at the top of the syllabus.