CS 747Software Verification Using Proof Assistants
- Units
- 0.50
- Level
- Graduate
- Faculty
- Mathematics
- Subject
- Computer Science
When it runs
- F24
- W25
- S25
- F25
- W26
- S26
- F26
- W27
- S27
Ran in 2 of the last 7 terms. Winter 2027: scheduled, 1 lecture section. Spring 2027: schedule not out yet.
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.
Winter 2027 sections
| Section | Class | Enrolled | Meets |
|---|---|---|---|
| LEC 001 | 6309 | 0 / 24 | Online or by arrangement |
Resources
Around the web
Found by uwloo’s link finder, which checks that each page names CS 747.
Reviewed on UW Flow
100% liked it50% easy75% useful
From 1 rating on UW Flow. Read them all on UW Flow.
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