Assignments

Use the Coq sources available from CMS, not from the public Software Foundations website. Changes are being made to exercises that are specific to CS 4160 Spring 2020.
Which exercises are required? TL;DR: complete the standard non-optional exercises. Every exercise is labeled as either standard or advanced. The standard exercises are what you need to solve; whereas, the advanced exercises are not required: you are welcome to dig deeper into the material with these, but they will have no effect on your score. There are two additional labels you will sometimes see on exercises: optional and recommended. “Optional” really does mean optional. You are free to skip or complete them, at your choice, with no effect on your score. “Recommended” doesn’t mean anything for the purposes of this course; ignore that particular label if you happen to see it, and complete the exercise according to whatever other labels it has.
Assignments are usually due at noon on Tuesday each week, but consult CMS for the official due date. To give you flexibility in managing your work schedule, late submissions will usually be accepted at no penalty until the late submission deadline given in CMS (usually, that will be 48 hours). After the late submission deadline expires, no further submissions will be accepted. Be aware that CMS does not allow any grace period for the late submission deadline, so you must be careful to submit well before it.
Solutions to an assignment will be released shortly after the late deadline, to help you on the next assignment.
Extensions are generally not possible in this course, because we release assignment solutions shortly after the late deadline. In addition, most assignments build conceptually on top of one another, so extensions would lead to a snowball effect. If you are having trouble keeping up with the assignments, please contact us sooner rather than later.
Compilation. Your solution must successfully compile from the command line against the test file(s) that we ship with the assignments. If it does not, and the grader can quickly fix the error (most likely by just admitting the claim), there will be a 15% penalty in addition to whatever points you lose as a result of the grader’s fix. If the grader can’t quickly fix it, there will be higher penalties—perhaps even a zero on the assignment.
Partial credit. There’s no feasible way to determine how “close” you are to a finished proof. So we don’t award partial credit for incomplete proofs. Instead, we break down large theorems into smaller claims (Theorem, Lemma, Example, etc.), and award all-or-nothing credit for proving those individual claims: either Coq accepts your proof, or it rejects it. You will know which case you’re in before you submit, so there should not be any surprises in grading.
Regrades. Regrade requests should be made in CMS before the deadline given in CMS. Please don’t use CMS regrade requests to ask for information—use office hours for that. Instead, use CMS regrade requests when you can demonstrate that something was graded incorrectly. On autograded problems, what matters is whether Coq acccepts your proof. We aren’t going to give any points back if your proof is rejected or incomplete. Please do remember to run make before submitting. The Graduate TA will process all the requests after the deadline expires. So, don’t worry if you don’t hear back right away.
Your lowest assignment score, excluding the last assignment of the semester, will be dropped.