CS 747Software Verification Using Proof Assistants
- Units
- 0.50
- Level
- Graduate
- Faculty
- Mathematics
- Subject
- Computer Science
CS 747 as listed in the Spring 2024 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 Spring 2024
- Graduate Calendar, Spring 2024The archived entry
- Requirements for Spring 2024Waterloo’s requisite checker
- Course outlinesSyllabi from past terms (UW login)
- UW FlowStudent ratings and reviews
- WClassesPast sections back to 2004, and who taught them