General Notes

Standard vs. Advanced Exams

• Unlike the homework assignments, we will make up two completely separate versions of the exam — a "standard exam" and an "advanced exam." They will share some problems, but there will be problems on each that are not on the other.
  You can choose to take whichever one you want at the beginning of the exam period.

Grading

• Meaning of grades:
  • A = mastery of all or almost all of the material
  • B = good understanding of most of the material, perhaps with a few gaps
  • C = some understanding of most of the material, with substantial gaps
  • D = major gaps
  • F = didn't show up / try
• There is no pre-determined curve. We'd be perfectly delighted to give everyone an A (for the exam, and for the course).
  • Except: A+ grades will be given only for completing the advanced track.
• Standard and advanced exams will be graded relative to different expectations (i.e., "the material" is different)

Hints

• On each version of the exam, will be at least one problem taken more or less verbatim from a homework assignment.
• On the advanced version, there will be an informal proof.

Expressions and Their Types

Thinking about well-typed expressions and their types is a great way of reviewing many aspects of how Coq works... (Discussion of Coq's view of the universe...)

Inductive Definitions

Tactics

Proof Objects

Functional Programming

Judging Propositions

More Type Checking

Good luck on the exam!