80-719 Interactive Theorem Proving

12 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: none listed

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