Formal Semantics of Programming Languages Fall 2018, Nanjing University

Assignments

• [12/01]: Complete all the definitions, lemmas and theorems for separation logic in SepLogic.v (i.e., replace all admitted parts with your own work), due by 12/14. Note: The Coq file requires Imp.v, which may in turn depends on other files. All the required files are in the Software Foundations package. You have to download the required files and submit them all together with your SepLogic.v file.
• [11/16]: Reynolds 3.1, 3.2 and 3.4, due by 11/23. Either submit in class, or email to TA. (Note that rem in Reynolds book means the more familiar mod operation. You should try to use rules in the lecture notes instead of those in the textbook, although most of them are the same)
• [10/26]: Exercises 2.1-2.5 and 2.9-2.10 of Reynolds. Due by 23:59pm, 11/09, (either submit in class, or email to TA).
• [10/12]: Assignment 2. Due by 23:59pm, 10/19, (either submit in class, or email to TA).
• [09/21]: 1) Finish all the exercises in Lists.v in the online textbook Software Foundations, vol 1 (see this page for details), due by 23:59pm, 09/30. (Note, you need to first compile Basics.v and Induction.v, which are needed in Lists.v. Finish the exercises inside the file and submit the complete file instead of these exercises only. It is your responsibility to locate every exercises and to make sure that no one is missed.) Submission: email the Coq source files to the TA <dingchao623+TA@gmail.com>;
  2) Reading: the first 6 chapters of Software Foundations, vol 1.

For each assignment, you get a grace period of 72 hours (with penalty over your grade) after the deadline. No submission will be accepted after the grace period, unless there are special reasons provided.

If your work is submitted within the first 24 hours after the deadline, the penalty is 90% (i.e. your score will be (your real score) * 0.9). Within 48 hours, 70%, and 50% for 72 hours.