Project

All information relating to the project can be found here.

Deadline

This deadline is strict, i.e., failure to submit all deliverables results in failure of the course.

All deliverables are due Friday, 7 November 2025 @ 14:00 (Delft Time).

You must upload them to WebLab.

Deliverables

In order to complete the project, you have to submit the following deliverables:

  1. A solution to the “Two Loops” exercise.
  2. A single Coq .v file containing the solution to your project.
  3. A corresponding .pdf written report.

Exercise "Two Loops"

Download the template for this exercise here .

You should put this file in the same directory as the PLF files, since it imports the material from that book. You are allowed to use all of that material.

Grading

Your solution must be essentially correct in order to pass the course. Your solution does not contribute in any other way to the grade you obtain.

Submit your solution on WebLab.

Project

You should pick one project from the following:

Each project consists of a basic part (divided in exercises) and several extensions, marked with their level of difficulty (easy, moderate, difficult, or very / extremely difficult). You should do

  • all the exercises (or as many as you are able to do), and
  • at least one extension.

Some remarks:

  • You are advised to first complete all the exercises before starting to work on an extension.
  • The level of difficulty of the chosen extension impacts your project grade, as described below.
  • You are allowed to use anything from the Coq standard library.
  • All of your code should be in one .v file.
  • You can adapt the signatures in the description files in trivial ways, e.g., by replacing Definition by Fixpoint or by putting arguments before the colon instead of after or vice versa.

Grading

Your Coq code will be graded on the following criteria:

  1. Correctness: Do the Coq definitions and lemmas correctly model the problem at hand?
  2. Completeness: Are all lemmas proven? Put differently, are any lemmas omitted or any proofs finished with Admitted. or stated with Axiom?
  3. Style: Does the Coq code follow sensible style guidelines? This includes, in particular, consistent indentation, proper use of parentheses, sensible variable names, proper use of implicit arguments, documentation where needed, appropriate use of automated tactics.
  4. Effectiveness: Are definitions and proofs carried out effectively? Put differently, are there redundant proof steps, uses of the induction tactic for lemmas that can be proved without induction?
  5. Difficulty: The level of difficulty of the extension you choose impacts your grade in roughly the following way:
    • easy extension: 6
    • moderate extension: 7
    • difficult extension: 8 Notice that picking a (very / extremely) difficult extension does not necessarily result in a high grade. Your project should also be good with respect to the other criteria.

Report

The written report should be in academic style (preferably typeset using LaTeX), written in English, and should include at least:

  1. Your name and student number on the first page.
  2. A small introduction with a description of the project you have chosen. You should not just copy the description from this document. This should also include a clear statement of which extension you have chosen.
  3. Most importantly, a description of the design choices you have made during the project, and the reasons for making them. If you had multiple solutions in mind, describe these, and explain why you picked the one that you used.
  4. Anything else you find noteworthy.

This list states the minimum requirement; if you have more material to discuss, please do so.

Some remarks:

  • You should not include unnecessarily long excerpts of Coq code in the report. Use only small fragments to illustrate a point.
  • Informal proofs should be formulated in a human-readable style.
  • A reasonable length for the report is about 3 pages. If you need more space, that’s fine, but keep in mind that conciseness is an evaluation criterion.

Grading

  1. Correctness: Is the problem correctly formulated? Are statements about logic, Coq, and other used resources correct?
  2. Completeness: Does the report discuss all the relevant design choices made in the project? Does it explain alternatives and reasons made for rejecting them?
  3. Conciseness: Does the report convey information efficiently?
  4. Style: Does the report use clear and simple language?

The report impacts your overall grade. If it:

  • is missing or has serious flaws: fail
  • covers the minimal content and satisfies most of the quality criteria: +0
  • covers the minimal content and satisfies all the quality criteria: +1
  • goes beyond the outlined quality criteria and is exceptionally insightful and clear: +2
  • demonstrates understanding far beyond the scope of the project: +3

Collaboration

The project is individual work.

  • You are allowed to collaborate with at most one fellow student, provided that:
    1. You acknowledge your collaborator in both your report and your Coq files, giving a precise description of the help provided by the collaborator.
    2. You carry out a different extension than your collaborator.
    3. You write the report by yourself.
  • You are allowed to consult academic literature provided you do not copy, you provide clear citations, and you clearly describe which ideas you have adapted from which source.
  • You are allowed to ask questions of a general nature, e.g., seeking clarification, in the corresponding Mattermost channel. You should not ask questions seeking help with the project.