Contacting the Course Staff
For email and the newsgroup: please allow about 24 hours for a response, except on weekends (see below). The staff do not work on the weekends. If you send something late Friday or over the weekend then you should not expect a reply before Monday. Never ever EVER call any staff at home.

Instructions for Submitting Assignments

In the first part of the semester, there will be a series of weekly machine problems (MPs). Each student is given an svn directory that needs to be checked out at the beginning of the semester to as follows: mkdir <working_directory> svn co https://subversion.ews.illinois.edu/svn/sp15-cs576/<your_netid> <working_directory> After the initial checkout, <working_directory> will contain a subdirectory assignments. Once an assignment has been announced, if you do an svn up you will add a directory named after the assignment (e.g. mp1). That directory will contain instructions for the assignment, plus a stub for each file you must turn in. To do an assignment, you will need to follow the instructions given in the directory for that assignment. Since the mps involve using Isabelle, by default you will need to do them on the ews linux machines. You may find it more convenient to download Isabelle to you own machine should you choose to work on your own machine. It runs under Linux, Windows and MacOS. To submit an assignment, once you have completed the necessry files as decribed in the assignment instructions, in the assignment directory or either of the parent directory or the gradparent directory svn commit -m "<your comment here>" You may restrict svn commit to a specific collection of files and directories by adding a list to the end of the command. You may do multiple commits; the version that is in the repositry at 11:59pm on the due date is that one that will be collected and graded.

Extensions

Each MP will normally have an automatic 48-hour extension with a penalty on that MP of 20% the total value of the assignment. If, for some reason, I cannot give such an extension for a particular MP, I will announce that when the MP is handed out. During the automatic extension, staff is not obliged to answer questions for that MP. You are on your own. Extensions without a point penalty for the first 48 hours and any extension beyond the 48 hours will only be granted under very unusual circumstances such as a medical or family emergency. A signed note from a responsible party will be required. If you do need such an extension for some legitimate reason, do your best to let us know as soon as possible, preferably before the normal MP deadline.

Regrade Policy

Our goal as the course staff is to grade your work carefully and accurately. Unfortunately, occasionally staff may overlook something, misunderstand an otherwise correct answer, or record a score incorrectly. This is where the regrade procedure steps in. In order to have your regrade considered you must provide the following: your netid; what assignment or exam question was graded incorrectly; and why you think your answer deserves more points than what the grader gave. You must also submit your regrade request for a particular assignment within one week of receiving grades for that assignment. It must be submitted directly to the course instructor, not to the TAs. Late regrade requests will not be accepted or read. Good reasons to ask for a regrade: You used a notation that was unfamiliar to the grader but is standard (e.g., in a textbook for one of your other courses). The grader recorded a score incorrectly. The problem was ambiguous (or just plain wrong), causing you to interpret it differently than the grader. The grader marked the problem wrong incorrectly. Bad reasons to ask for a regrade: Part of your answer "matched" the answer given in the solution. A partially correct answer is still wrong. "The difference between an almost right word and a right word is the difference between a lightning bug and lightning." -- Mark Twain You wrote down two or more answers, only one of which was correct. Never put more than one answer for a question unless we tell you that such a thing is legitimate. You expended a lot of effort answering the problem. We are measuring mastery, not effort. You wrote something down.

Collaboration

You are allowed to collaborate on the machine problems (MPs), in order to figure out how to solve the problem, resolve things you don't understand, and help each other track down errors or bugs. Nevertheless, you must each write and test your code separately and submit your own MP. If your collaboration extended beyond understanding for what the problem was asking, then you should note on your assignment with whom you collaborated, and the nature of the collaboration. As always, you are subject to the rules for plagiarism. We allow you to collaborate for several reasons: all research done indicates that students learn more when they are allowed to work together; our own ability to respond to student questions is increased because your peers are able to give help. However, you have to collaborate intelligently in order to get the most out of it. If you ask a friend to describe the solution completely to you and then write it down, you will get the credit but you'll fail to have learned the concepts when you need to use them in carrying out your course project. If you copy a friend's solution directly or substantially, that will be considered cheating, unless you give a clear cite of your source. If you work as a group, each writing part and sharing it with the others, that is also considered cheating, unless your cite all members from whom you copied. The penalties for being discovered cheating are described in the next section, below. If you offer your solution for others to copy, you should protect yourself from being accused of cheating by reporting this as well. Then, if some of those to whom you have lent your work fail to cite you, you will be protected from cheating accusations (unless they also claim they lent the same problem to you). If you copy your solutions from friends or other sources, you must cite your source. Think of MPs as warm-up execeises for your course project. If you do not lay the foundations well with the MPs, you will have increased difficulties doing the work involved in the course project. On the course project, you are allowed to work in groups of two or three. All groups must be reported to me at the start of the project portion of the class. Students working in groups are expected to take turns describing their group project's progress and difficulties.

Policy on Academic Integrity

We will be looking for cheating on both MPs and project write-ups. The penalty for being caught cheating on an MP -- copying someone else's solution for part or all of an MP without citation, or imporperly copying or paraphrasing work of another author without appropriate declararion and citation -- is that you will receive a negative score for that MP equal to the value of the MP. An act of plagarism on course project will minimally result in the lost of a letter grade for the course. A second act of cheating or plagarism will result in an F in the course. Moreover, if you cheat a second time, both cheating episodes will be reported to the department.

Grading
Our goal is to have grades back to you as soon as possible. In practice, this will probably take about a week for each assignment. When your homework is graded, it will be returned to your svn repository with your MP grade and comments on how you could have improved it or what you did wrong. Grading Breakdown Work Weight(4 cr) Machine Problems (combined) 33% Course Project 67%

Textbooks
Recommended: Programming and Proving in Isabelle/HOL by Tobias Nipkow Isabelle HOL: A Proof Assistant for Higher-Order Logic" by Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Published by Springer-Verlag. A tutorial on the use of Isabelle/HOL. Please use the online version dated August, 2014. It is also available through the Isabelle distribution.
Recommended: Tutorial on Isar Tutorial on Locales Tutorial on Type Classes Tutorial on Function Definitions