skip to main content
CS 128
Interactive Theorem Proving
9 units (3-0-6)  | second term
Prerequisites: CS 4 or instructor's permission.

This course introduces students to the modern practice of interactive tactic-based theorem proving using the Coq theorem prover. Topics will be drawn from logic, programming languages and the theory of computation. Topics will include: proof by induction, lists, higher-order functions, polymorphism, dependently-typed functional programming, constructive logic, the Curry-Howard correspondence, modeling imperative programs, and other topics if time permits. Students will be graded partially on attendance and will be expected to participate in proving theorems in class.

Instructor: Vanier