80-419 Interactive Theorem Proving

9 units, Carnegie Mellon University

Interactive theorem proving involves using computational proof assistants to verify that mathematical proofs are correct, or to verify that hardware and software designs meet their formal specifications. This course uses a new interactive theorem prover, Lean, to explore this new technology and its logical foundations. We will study dependent type theory, a powerful and expressive language for representing mathematical objects, algorithms, and proofs. We will also consider automated methods that can be used in support of formal verification, including propositional, equational, firstorder, and higherorder methods, as well as decision procedures for real and integer arithmetic.

Prerequisites: 80-211 or 21-300 or 15-317 or 80-310

Courseweave needs JavaScript to show sections, workloads and planning tools.