CS 6115 - 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.

Deadlines

Proposal: October 17
Check-In: November 19
Final: December 16 @ 4:30pm (determined by the register)

Requirements

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.

Partners

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.

Grading

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

Proposal: 5%
Check-In: 20%
Final: 75%

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.

Proposal

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

Team Formation

If you plan to work with a partner, indicate your partnership on CMS.

Proposal

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

The members of your team, including their names and NetIDs.
Logistics plan, a brief description of how you plan to manage details like version control and communication with your team (if you have a partner).
A proposal for your system. Summarize the system you intend to build. Tell us what will be the most important functionality of your system. This summary should be about one page long. Provide:
- A short statement of the core vision or key idea for your system.
- A short list of the key features of the system.
- A narrative description of the system you intend to build, prove, formalize, etc. Go into enough detail that, if your proposal were given to another team, and that team were never allowed to talk to you, they would still understand more or less the functionality that you have in mind.
A roadmap for your project. I recommend structuring the project around a relatively easy to achieve baseline, and several extensions.
A preliminary design sketch for your project. Spend some time thinking through what you are going to need to build, formalize, prove, etc. Of course, your plans will evolve throughout the project. But it’s good to have thought up front about what seems necessary.

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. There is no need to upload this agreement to CMS, although you’re free to include it if you like.

Check-In

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.

Prototype

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 prototype.zip on CMS, and include instructions for how to build and run your code in a README file.

Blog Post

We’re also asking you to put together a brief blog post for the whole class to read. This post can be short and should be written so that everyone in the course can understand it. You may include accompanying graphics if helpful. At this stage, your blog post only needs to cover your the topic of your project and perhaps a few highlights of your technical approach.

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

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:

Vision: In one paragraph, what is your current vision for the system you are building? How has it evolved?
Summary of progress: Write a one or two paragraph description of what your team accomplished so far. If you have an initial demo, what functionality does it show?
Activity breakdown: If you are working with a partner, give a bulleted list of the responsibilities that team member had and the activities in which they participated during the sprint.
Productivity analysis: How productive were you? Did you accomplish what you planned? Were your estimates of what you could do accurate, or far off? Write a paragraph addressing those questions.
Grade: Give your team a scope grade for this phase: Satisfactory, Good, or Excellent. Your grade should be based on your experience of those levels of scope in the assignments thus far in this course. Write a paragraph or two providing a detailed justification of why you gave yourself that grade. Please be honest: we want you to reflect candidly on your progress. Your grade for the Alpha phase is not going to be based on what you self-assign here.
Goals for next phase: Set goals for the final phase, corresponding to what you believe would constitute Satisfactory, Good, and Excellent scope for that sprint.

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

Final

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.

Report

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.

Demo

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:

Vision: What are you trying to achieve? It’s fine to re-use text from your project report if helpful, but remember you are writing for the whole class, not just the instructor!
Achievements: What did you achieve? Show us your system – theorems or a screenshot might be helpful.

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).