Interactive Theorem Proving
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.
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.