CS 358. Lecture Topics and Suggested Reading

• 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 ...