Expectations about the midterm project

The midterm project is in two parts:

• the project proper (as a .v file), carried out in groups, and
• a report (as a .pdf file), concisely written in groups.

It will then be followed by an oral exam conducted through Zoom where we will talk about the project and probably write a program and prove a property about it.

The reading grid for grading

The .v file, the form:

• does it load completely?
• is it indented in the standard way (programs, propositions, and proofs)?
• does it use admit, Admitted, or Abort?
• does it contain comments, and if so of which nature (indicative / analytical)?

The .v file, the content:

• are there unit-test functions before all the implementations?
• are the unit-test functions the same as the ones in the given resource file, or are they expanded?
• is at least one unit test proved to be sound with respect to the specification?
• are all the implementations tested?
• are all lemmas applied to all their arguments?
• are fold-unfold lemmas properly defined and properly used?
• do the proofs focus on all subgoals?
• are any corners cut (e.g., reflexivity is used on non-syntactic equalities)?
• are all tasks carried out?
• are routine proofs carried out routinely?
• are simple things done simply?
• are there any extras?

The .pdf file, the form:

• is it original?
• front page: incomplete / out of scope / standard / clever
• page numbers: yes/no
• table of contents: present or absent / uninformative / standard / clever and telling
• introduction: minimalistic / telling / amazing
• each section:
  • with an introduction and a conclusion / without
  • with just code / with a narrative interspersed with code
  • with everything, torrentially / with brevity, measure, or even concision
  • with no narrative / an ordinary narrative / an outstanding narrative
  • with no quotes / with fitting quotes / with ill-fitting quotes
• conclusion: minimalistic / telling / amazing
• remarkably short / medium size / enormous size
• incomplete / OK / with pluses (optional proofs or any extra thoughts, examples, or proofs)
• was the report spell-checked?

Version

Created [22 Feb 2024]