CS 747Software Verification Using Proof Assistants
- Units
- 0.50
- Level
- Graduate
- Faculty
- Mathematics
- Subject
- Computer Science
CS 747 as listed in the Fall 2026 Graduate Calendar. The main page has the current version, when it runs, and seats.
Dependent types and the Curry-Howard correspondence (proofs as programs); constructing inductive datatypes and proofs by induction; relations; equality; logical connectives and quantifiers; decision procedures; the simply-typed lambda calculus and theorems about it; intrinsically-typed representation; verification of elementary algorithms.
Prerequisites
None listed.
Antirequisites
- Not completed nor concurrently enrolled in:
Leads to
No course lists it as a requisite.
Check it elsewhere for Fall 2026
- Graduate Calendar, Fall 2026The official entry
- Requirements for Fall 2026Waterloo’s requisite checker
- Schedule of Classes, Fall 2026Instructors, rooms, live seats
- Quest Class SearchWhere you enrol
- Course outlinesSyllabi from past terms (UW login)
- UW FlowStudent ratings and reviews
- WClassesPast sections back to 2004, and who taught them