Course Project

The course project is an open-ended Coq development experience. Think of it as an activity that takes place instead of a final exam and that requires corresponding intensity. There will be three milestones in the project: Proposal, Check-In, and Final. For the Proposal milestone, you will optionally form a team and propose the project you want to complete. For the Check-In milestone, you will build out some part of of your system and report on your progress. For the Final milestone, you will complete your project and write a final report.



The primary educational objective of this project is for you to gain experience with certified systems, either in a theoretical or application context. You can implement a data structure, an algorithm, or a full-blown system in Coq and proof it correct; you can investigate techniques for developing systems in Coq; or you can reproduce ideas from a previously-published papers. It’s also fine to draw on your research, but please indicate which portions were done fresh for CS 6115.

Size: Ideally, should aim for at least a few thousands lines of Coq code.

Source control: You are encouraged to use Git to manage your source code. You are welcome to make your project work public.


You are welcome to do the project solo or with a partner. However, if you have a partner, both members of the team must contribute to the project.


The project is worth 40% of the final grade, and will be broken down as follows:

Why is the Final phase worth so much more than the earlier phases? It’s not because you should do five times the work all at the end: it’s because I don’t want any initial stumbles to have too great of an impact. I encourage you to work at a consistent pace throughout the project.


Your task in this milestone decide what you want to build. There is only one deliverable: the project proposal.

Team Formation


Submit a short (~1 page) document containing the following information:

Team Expectations

Teamwork isn’t always easy. But when teams work and communicate well, the benefits more than compensate for the difficulties. One way to improve the chances that a team will work well is to agree beforehand on expectations. If you are working with a partner, we recommend creating a Team Expectations Agreement. Make your expectations fairly thorough without being unrealistic. For example, “We will each solve every part of the assignment completely before we get together” or “We will get 100% on every assignment” are probably unrealistic. You might want to reference the section below on “Teamwork and Roles” as part of your expectations. There is no need to upload this agreement to CMS, although you’re free to include it in your charter if you like.


Your task in this milestone is to have made some initial progress on your project. That is, you should build some functionality, test it, submit your source code and a progress report, as well as a brief blog post, as described below.

Coding Sprint

For the Check-In phase, your technical goals can be extremely modest. However, you should aim to get some functionality running. In most cases, this will typically consist of an initial implementation of some piece of the overall system that has been prototyped, plus some initial validation. In any case, the key thing is to have something that runs.

You should submit your code as a Zip file named on CMS, and include instructions for how to build and run your code in a README file.

Progress Report

You’ll put together a self-evaluation of your progress at the end of the Check-In phase by writing a brief progress report. Your report should be approximately 1 page long. It should contain the following information:

You should submit your progress report as a PDF named report.pdf on CMS.


Your task in this final milestone is to finish your project. You’ll complete any required coding, documentation, and testing, and write a brief report. Your sumbission must provide a README file that describes how to build and run your code.


You’ll put together a self-evaluation of your progress at the end of the Beta phase by writing another brief progress report. Your report should be approximately one or maybe two pages long. It should contain the same information as for the Check-In phase. Instead of “Goals for next phase” please identify some possible next steps for this project, were you to continue it. You should submit your progress report as a PDF named report.pdf on CMS.


Design a demo for your system and put together clear instructions for how to run it. The demo does not need to be sophisticated (but it should be more than just running unit tests). It’s fine to have both positive and negative examples (e.g., here’s a program that does not pass the type checker). However, the demo should illustrate the main features of your system. Make sure that all required inputs are provided, including any interactive input from the user.

Blog Post

We’re also asking you to put together a brief blog post for the whole class to read. This post can be as short as a few hundred words. It should be written so that everyone in the course can understand it. You may include accompanying graphics if helpful. Your blog post should cover:

You should format your blog post in Jekyll-flavored Markdown and submit a Zip file named on CMS that contains a file with your blog post, along with any other supporting files (e.g., images).

Acknowledgment: The structure of this document is adapted from the CS 3110 project. The list of sample team expectations above is from the University of Waterloo Centre for Teaching Excellence, citing Levin and Kent (2001).