Course Overview
This course provides a hands-on introduction to programming and
verification using proof assistants.
Prerequisites
Students taking this course are expected to have substantial prior
programming experience and be familiar with basic mathematical
concepts such as functions and induction proofs.
Course Meetings
Lectures meet at 12:30 PM on Wednesdays.
The location can be found on Quest.
Coursework
Breakdown of Marks
| Class participation |
5% |
| Programming assignments |
45% |
| Course project |
50% |
| Total |
100% |
Participation
Students are expected to attend all lectures and participate in discussions.
Programming Assignments
Submit your completed assignments to Marmoset by 11:59 PM (ET) of the due date.
Course Project
The main goal of the project is for you to practice using a proof assistant
in a theoretical or application context.
You can use the proof assistant to formalize any interesting aspect of
computing (data structures, algorithms, protocols, language designs, compilers, runtime systems, hypervisors—you name it!) and prove properties about them.
You can also investigate formalization techniques or even extensions to
proof assistants themselves.
It is acceptable (and a good idea!) to draw on your own research, but the work that is done fresh for this course should be clearly identified.
It is also fine to use proof assistants other than Rocq (e.g., Lean,
Agda, Isabelle/HOL, Dafny, F*) if you have experience with them.
As a rule of thumb, a project should be at least as substantial as a
few thousand lines of Rocq code.
By February 14, submit a project proposal to Marmoset.
The proposal should include the following information:
- A short paragraph on the core vision or key idea of your system.
- A short list of the functionalities you intend to formalize and the
properties you intend to prove.
- A more detailed description of the project. Go into enough detail
that your peers in the class can more or less understand what you
are doing just from the proposal.
- A roadmap of how you plan to execute the project.
Sketch out work items.
Structure your project as a list of milestones and give time
estimates.
This will probably take two pages (excluding references).
On March 26, you will give a short presentation on your project to
the class.
Use a few PDF slides to explain the project at a high level.
Report on your progress, and set goals for the final stretch.
You should aim to at least get some functionality running by this stage;
this typically means you have prototyped some piece of the entire system
and have done an initial validation.
If you have a demo, show it!
Showing any interesting aspects of your formalization effort will also
be welcome.
Consider the presentation as a forcing function to get you to make
progress on your project.
Submit your slides to Marmoset by noon on the day of the presentation.
By April 19, submit a final report to Marmoset.
The report should describe what you have done for the project,
including an overview of the system and of the approach you took to
construct a machine-checked proof.
Discuss interesting aspects of your work, challenges you faced,
and design decisions you made.
Reflect candidly on what you have achieved and what you have not.
Reflect on what you have learned from this experience.
Identify any future work that could be done to extend or improve your
project.
This will probably take five or more pages.
By April 19, submit the source code of your project to
Marmoset as a zip file.
Include enough documentation so that someone can explore and build on
your submitted source.
Include a demo for your system and clear instructions for running it.
The demo should serve to illustrate what you have achieved.
The proposal and the final report should be in the form of
PDF files typeset with the acmart format
and the acmsmall subformat.
All submissions are due at 11:59 PM Eastern Time on the respective due dates.
Course Staff
Other Notices and Statements