CS 842: Dependent Types and Software Verification

A revised version of this course is now available as CS 747 (Fall 2021).

This is the homepage for CS 842 at the University of Waterloo (Fall 2019). Although this is a graduate course, undergraduates may take it with permission of the instructor and a CS advisor, and it may be used to fulfil undergraduate fourth-year course requirements. (Added Sept 9: the calendar says 600- and 700-level courses can be so used, but it doesn’t mention 800-level, so this is not guaranteed.)

Instructor: Prabhakar Ragde (plragde at uwaterloo dot ca).

Lectures: Tuesdays and Thursdays, 11:30am-12:50pm, DC 2568. Lectures start Sept. 4 and end Nov. 28.

Office hours: Thursdays 10am-11am, DC 1314, or by appointment. Temporary changes to these times will be announced on Piazza.

Added August 27: Introductory video prepared for the SCS Grad Office now available (MP4, 14 mins, 269Mb).

Added Sept 5: I will get permission numbers from the Grad Office on Tuesday, Sept 10. If you are not enrolled and wish to be, please send me a fresh email before then. Future announcements will be made on Piazza.