CMSC 838E: Verified Compilers🔗

Spring, 2026

Lectures: Tuesday & Thursday, 2:00-3:15pm, CSI 2120

Professor: David Van Horn, TA: Benjamin Quiring

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.

Communications: Course communication is handled through Piazza.

Assumptions: As a graduate-level course, the major assumption is that you are self-directed and motivated to pursue your own educational goals and that you can collaborate with others. Coming in to this course, you should know how to program in a functional programming language like OCaml and have some familiarity with programming in C and Assembly. The course is built upon the foundation of CMSC 430, but it’s not assumed you’ve taken the course; only that you can work through the material quickly.