| Course Description |
|
The course will come in two parts with the divide at the
middle of the term. The first half of the course will have
a standard lecture format where we will cover the language
and logics of the theorem prover Isabelle, namely Simple
Type Theory, also know as Higher-order Logic and how to use
the theorem prover Isabelle-HOL, including how to model
complex systems in Isabelle-HOL and formally prove
properties of them. During this period, there will be one
homework set per week. (Having taken CS 421 Programming
Languages and Compilers will be a help because the exposure
to functional programming.)
During the first half, some papers and possible topics for
projects will be posted and students will be asked to either
pick one or propose something of their own (perhaps out of
another course being taken or something that might tie in
with their research objectives.) The proposals must be
submitted before the end of sixth week, and will be vetted
to try to suggest when they are over-ambitious, or possibly
under-ambitious. Projects may be solo or done by small
groups. The size of the project should reflect the size of
the group.
In the second part of the course, there will be weekly
presentations of the progress and difficulties incurred on
the projects, and discussion with the whole class of
approaches to over come those difficulties. Students
attending asynchronously will be expected to submit a
written presentation ahead of the class time. There
generally is enough in commnon among various projects that
the techniques to help one are what are needed by about half
the class at any given time.
At the end of the course, for each project, I will ask
each group member to give a separate write up of their
contributions and give a brief verbal final presentation.
Mostly, the level of difficulty will be determined by the
difficulty of the project you choose. Students will learn how to model projects
formally in higher-order logic, accurately state
properties that are required of the model, and carry out
some moderately complicated proofs. Inductive methods and
recursion will be an ever present theme. Final grade will
be one third homework and two thirds project.
|
| Objectives |
Students taking this course can expect to acquire the following:
- a thorough understanding of logic, particularly
higher-order logic and how formal logical proof relates to
mathematical problem solving;
- an understanding of how to model problems from various
areas in computer science in higher-order logic;
- the ability to accurately state properties that are
required of the model, and carry out moderately complicated
proofs of these properties.
|
| 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
|
-
Assignments will be distributed and collected in
PrarieLearn.
To log in, choose University of Illinois
Urbana-Champaign (UIUC)
-
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.
-
I am trying to get Isabelle installed in
PrairieLearn. If this succeeds, it will be announced on
the main webpage.
|
| 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% |
|
|
|
