CS 358. Lecture Topics and Suggested Reading
- Apr 5. Introduction to Linear Logic. Here are some general references
- 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
- 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
- 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
- June 5. Plan: Proof games that are hard to even come close to
- June 7. Plan: Reports: Kathleen Fisher and Julie Zelenski, Dialogue
games, Pi-calculus and PCF. Reference: Reference: Hyland and Ong, Dialogue