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.

Announcements

• 4/14 The tenth assignment is out. Continue reading 12.
• 4/3 The ninth assignment is out. Read the HoTT Book, esp. 1.12, 2.1–2.6, 3.1–3.4.
• 3/31 The eighth assignment is out. Continue reading 11.
• 3/22 The seventh assignment is out. Continue reading 9–10.
• 3/2 The sixth assignment is out. Continue reading 8, start thinking about final projects.
• 2/14 The fifth assignment is out. Continue reading 6–7, do exercises (especially 6.4)
• 2/8 The fourth assignment is out. Continue reading 6, and prove some theorems.
• 2/4 The third assignment is out. Continue reading 3–5 with exercises.
• 1/27 The second assignment is out. Continue reading 2–3 with exercises, start chapter 4.
• 1/17 The first assignment is out. Read chapter 1–3 of the tutorial and do exercises in chapter 2.
• 1/16 Welcome to 15–815!

Lectures

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

Contact Information

Instructors

• Prof. Edmund M. Clarke
  • e…@cs.cmu.edu
  • Office: GHC 9231
  • Phone: (412) 268–2628
  • Office hours: By appointment
• Prof. Jeremy Avigad
  • a…@cmu.edu
  • Office: Baker Hall 161D
  • Phone: (412) 268–8149
  • Office hours: By appointment

Teaching Assistant

• Soonho Kong
  • s…@cs.cmu.edu
  • Office: GHC 9232
  • Office hours: By appointment

Course Secretary

• Charlotte Yano
  • y…@cs.cmu.edu
  • Office: GHC 9229
  • Phone: 412–268–7656