Quizzes

There will be three in-class, closed-book quizzes during the semester. Quizzes are intended to confirm your understanding of topics studied in labs.

Quizzes are held on Moodle, on your own laptop. On quiz days, come on time, turn off all AI, chats, etc. (you may not consult any external materials, search engines, AI agents, tea leaves, or other students).

Exam lab

The last lab of the semester is an “exam lab”.

In week 8 (April 16) you must attend the Thursday lab session and submit your work-in-progress code at the end of the session. You may then finish the lab at home. Your score will be a weighted average of your score at the end of the lab session and your final score at the end of the week.

Checkoffs

You will have one “lab checkoff” in the semester.

Checkoffs are in-person examinations lasting approximately 8-10 minutes, during which you present your lab solution, along with an English explanation of your proofs. Each student will have one checkoff during the semester. You must follow roughly the following template:

• 1 minute overview of your submission (scroll through with the instructor giving you the check-off)

• 7 minutes deep dive into one interesting theorem of your choice:

  • 3 minutes on the proof plan / big idea / key lemmas, without looking at code and without Rocq jargon (no “tactics”, “destruct”, “repeat”, …). Pretend you're talking to a computer scientist who knows nothing about Rocq.

  • 4 minutes on the code, showing how it follows the logic of your proof plan.

Your proof plan should be written down as a standalone comment within your source file, submitted by the usual deadline.

Team registration

Start by registering your team on Moodle. Your team must have three members: if you cannot find a team, post on Ed. If your topic requires that you work alone, find a different topic (if you must request an exception, please do so by sending the staff a private message on Ed).

Project proposals

Aim for 400 words (do not exceed 500), and assume an informed (but not expert) reader. Submit your proposal as a public Ed post (not question) in the “Project tracking” category. A good project proposal should follow the format of an “extended abstract”, with the following parts (roughly):

Introduction / problem statement (1-2 paragraphs)

State what the problem is (a good example helps a lot) and (ideally) why it matters. Keep it short and to the point: give enough context to understand, but not more. Cut out the soaring rhetoric. It should be clear from the introduction what it means to solve the problem.

Proposal (2-4 paragraphs)

Summarize what you plan to do: how will you approach the problem? What deliverables (artifacts, proofs, ...) will you produce? What interesting challenges do you foresee?

Timeline and responsibilities (1 paragraph)

Break down your project into small components and milestones, then estimate how they depend on each other and how long each will take. Organize the milestones on a timeline. Clarify who will do what, and how you will organize the work of your group.

Weekly updates

Your team will update the rest of the class on your progress every week by creating a new comment thread every week below your proposal post.

All team members should contribute to each update, but the update should be written and posted by just one of the team's members each week. Each team member should post an equal number of updates (2 per person).

Use the following template (summary of this week's result + one highlight / thing you learned + plans for next week):

Week 9 update

Status update: We have completed the proof of three of the four lemmas that we highlighted last week: tree_rev_involutive, insert_delete_cancel, and rotate_lookup_iff […].

One thing we learned: The last lemma (insert_insert_comm) turned out to be wrong, because insertion order affects the shape of the tree: […]. We have rephrased it to use a new equiv predicate: […].

Future plans: Next week, we plan to complete insert_insert_comm and to start connecting the functional model with the imperative implementation by setting up the Hoare logic.

Presentation

In the last week of class, you will present your work to your classmates.

Aim for 10 minutes, plus 5 minutes of questions / interruptions. The structure of the talk should be similar to that of the final report (below), skipping the timeline and related-work parts.

All students should contribute equally to the presentation.

Final report

Aim for 1600 to 1800 words (about four pages; do not exceed 2000 words), plus code listings and figures. Assume an informed (but not expert) reader. Submit your report as PDF, using the provided template. The structure is similar to that of a tech report:

Abstract (1 paragraph)

A one-paragraph condensed version of the motivation and results.

Keywords

One line, naming the course techniques and concepts that you used in your project.

Introduction / Motivation (1/2 page)

This should be an expanded version of the proposal's introduction.

Approach (2 pages)

Summarize how you solved the problem. Aim to present the general approach and the most challenging aspects in enough detail that someone else could reproduce your work, and try to justify non-trivial design choices. Show concrete examples of Rocq definitions.

Results (3/4 page)

Clarify exactly what you achieved and what the limitations are. Show relevant data: concrete examples of Rocq theorems, benchmarks, ….

Timeline (1/4 page)

Compare the actual development of the project to your original timeline. Highlight the main divergences. Clarify who did what.

Related work, future work, conclusion (1/2 page)

Highlight related efforts, and suggest interesting continuations of your work.