Expectations about the term project

The term 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.

Time permitting, this term project will 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 the standard naming convention?
• 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 all the implementations tested?
• are all induction hypotheses applied to all their arguments (if any)?
• are fold-unfold lemmas properly defined and properly used?
• do the proofs focus on all subgoals?
• are any corners cut (apply used on a bi-implication, discriminate used without argument, destruct or case used without as, simpl used without argument, etc.)?
• 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

Fixed “are all lemmas applied to all their arguments?” to become “are all induction hypotheses applied to all their arguments (if any)?” [05 May 2025]

Created [11 Apr 2025]