## CS 358. Lecture Topics and Suggested Reading

Spring 1995

- Apr 5. Introduction to Linear Logic. Here are some general references
available electronically:
- P. Lincoln's SIGACT
News column on linear logic,
- A. Scedrov's Brief
Guide to Linear Logic and
- A. Scedrov's Marktoberdorf
Summer School Notes on Linear Logic .
- Apr 10-12. Basic proof theory: sequent calculus and cut-elimination
for classical and intuitionistic logic. Introduction to proof system for
linear logic.
- Handout based in part on Girard et
al.,
* Proofs and Types. *
- Recommended additional reading: Chapters 2 and 5 of
*Proofs and Types.
*
- Apr 17. Lecture canceled.
- Apr 19. Intuitive explanation of connectives of linear logic. Decision
Problems.
- Handout on sequent calculus for linear logic.
- Draft reading list for future topics.
- Apr 24. (Lecture by Andre Scedrov) Overview of decision problems, permutability
of rules in cut-free proofs, NP-completeness of multiplicative fragment
with no propositional variables. (Proof due to Lincoln
and Winkler; slides distributed Apr 26). Exercises.
- Apr 26. Phase semantics. Handout with exercises.
- May 1. Undecidability of full propositional linear logic. (Presentation
by P. Lincoln, based on LMSS.
) Undecidability of second-order linear logic without exponentials
using phase spaces. (Based on Lafont
undecidability paper; see also Lafont
and Scedrov. )
- May 3. Introduction to games. Reference: Blass, Is
game semantics necessary?
- May 8-15. Continue discussion of Blass article; cover main topics from
Abramsky and Jagadeesan, Games and full completeness
for multiplicative linear logic.
- May 15-17. Proof games and relation to stochastic complexity classes.
Reference: Lincoln, Mitchell and Scedrov, Stochastic interaction
and linear logic.
- May 22. Linear lambda calculus. Handout.
References: Abramsky, Computational
interpretation of linear logic. Lincoln and Mitchell, Operational
aspects of linear lambda calculus.
- May 24.
*Plan: *Francois Guimbretiere, report on proof nets. Continue/complete
discussion of linear lambda calculus.
- May 29.
*Memorial Day. No meeting. *
- May 31. Report 1. Oliver Duschka, coherent spaces. Report 2. Vitaly
Shmatikov, fair games. Reference: Hyland and Ong, Full
completeness ...
- June 5.
*Plan: *Proof games that are hard to even come close to
winning.
- June 7.
*Plan: *Reports: Kathleen Fisher and Julie Zelenski, Dialogue
games, Pi-calculus and PCF. Reference: Reference: Hyland and Ong, Dialogue
games ...