DRAFT
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

Please Note

The online version of the Caltech Catalog is provided as a convenience; however, the printed version is the only authoritative source of information about course offerings, option requirements, graduation requirements, and other important topics.