15-816 Linear Logic
Assignments

Assignments generally are given out Monday and are due the following Monday.
Assignments 1-6 are individual assignments. They must represent your own work. You may consult any publicly available resources such as papers, reports, or lecture notes, but you must explicitly credit such external resources in your answers.
The status of assignments 7-9 will be announced later.
Homeworks may require an implementation, or simply a write-up with LaTeX or with pencil and paper.
If you want to typeset your answers, some sample LaTeX lecture notes and necessary style file are posted in the misc directory.
Emphasis is on correctness and elegance. Some assignments may be very difficult. If you cannot do them, write down your thoughts, but never hand back an incorrect "proof".
Written homeworks are due at the beginning of lecture on the due date. They should be handed in before lecture or submitted as PDFs via email to the instructor.
We will try our best to return graded homework during the lecture following the due date.

Out		Assignment	Reference	Due

Jan	26	L1.4 (peg solitaire), L1.5 (blocks world invariant), L1.6 (truman quote), L2.3 (alternative -oL rule), L3.2 (alternative &L rule), L3.10 part (viii) only (interactions of -o and +)	LaTeX Support	Wed	Feb	1
Feb	8	L4.3 (unbound output), L4.4 (coin changing process), L5.3 (bang interactions), L6.3 (existentials), L6.4 (atm)		Wed	Feb	15
Feb	15	L7.3 (cut for alternative -oL rule), L8.3 (unrestricted implication), L9.1 (chaining disjunction), L9.2 (persistent focus)		Wed	Feb	22
Feb	26	L10.2 (i) and (iii) only (proof terms), L10.3 (alternative bang elimination), L10.4 (from sequent calculus to natural deduction), L11.2 (multiplicative unit), L11.3 (unrestricted functions)		Fri	Mar	2
Mar	28	Assignment 5		Mon	Apr	9
Apr	12	Assignment 6		Wed	Apr	18
Apr	19	Assignment 7		Wed	May	2