CMU 15-815 Interactive Theorem Proving

15–815 Interactive Theorem Proving

Spring 2015 Semester Computer Science Department

Course Description

This course is an introduction to interactive theorem proving using dependent type theory. Topics include dependent data types, type theory as a proof language, declarative vs. tactic-based proof style, inductive data types, encodings of structures and type classes, classical vs. constructive logic, homotopy type theory, and elaboration and unification algorithms. The course will be based on a new open-source theorem prover, Lean, developed at Microsoft Research.



Friday from 3:30 to 5:00 pm in NSH 3002.

Contact Information


Teaching Assistant

  • Soonho Kong
    • s…
    • Office: GHC 9232
    • Office hours: By appointment

Course Secretary

  • Charlotte Yano
    • y…
    • Office: GHC 9229
    • Phone: 412–268–7656