Build Your Own Proof Assistant

The goal of this course is to build a proof assistant together. A general-purpose proof assistant is a lifetime project, so we will instead target some specific domain and audience, effectively building a domain-specific proof assistant. We will collectively decide which domain and audience to target in the first week.

For more details on the format, grading, and schedule, please request access to this Google Doc if you are taking the course!