|
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.
Policy for late submission
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.
back