Instructor:
Steve Zdancewice-mail: stevez (AT) cis.upenn.edu
office hours: Thursdays 4:00-5:00pm (and by appointment) Levine 511
Course information:
time: MW 3:00-4:30room: Towne 309
Topics: Linear Logic
- Proof Theory
- Term Languages
- Semantics
- Applications
Reading and References
- Linear Logic Girard 1987
- Linear Types Can Change the World! Wadler 1990
- A judgmental analysis of linear logic Chang, Chaudhuri, and Pfenning 2003
- CMU's 15-816: Linear Logic Frank Pfenning
- Computational Interpretations of Linear Logic Samson Abramsky 1992
- Call-by-name, Call-by-value, Call-by-Need, and the Linear Lambda Calculus Maraist, et al. 1995
- Automated Theorem Proving 15-815: Automated Theorem Proving, Lecture Notes by Frank Pfenning 2004
Grading Criteria
- 50% Participation
- 50% Course projects (group projects)
Lecture Topics and Notes
Note: The following schedule is tentative!| Date | Topic | Handouts / Notes |
|---|---|---|
| 1/13 |
||
| 1/15 |
Introductions: Linear Logic | |
| 1/20 |
MLK Day - No Class | |
| 1/22* |
POPL - No Class | |
| 1/27 |
Intuitionsistic Linear Logic: Multiplicative Fragment | |
| 1/29 |
Intuitionistic Linear Logic: Additive Fragment | |
| 2/3 |
Intuitionistic Linear Logic: Persistent Judgments | lecture notes on ILL |
| 2/5 |
Proof Terms for ILL and Operational | |
| 2/10 |
Operational Semantics, CBN, CBV, Translations | |
| 2/12 |
Normal Proofs (part 1) | |
| 2/17 |
Normal Proofs (part 2) | Project Proposals Due |
| 2/19 |
Sequent Calculus formulation of ILL | lecture notes on ILL (updated) |
| 2/24 |
Completeness of Sequent Calculus I | |
| 2/26 |
Completeness of Sequent Calculus II | |
| 3/3 |
Classical Propositional Logic | |
| 3/5 |
Classical Linear Logic | |
| 3/10 |
Spring Break - No Class | |
| 3/12 |
Spring Break - No Class | |
| 3/17 |
||
| 3/19 |
||
| 3/24 |
||
| 3/26 |
||
| 3/31 |
||
| 4/2 |
||
| 4/14 |
||
| 4/16 |
||
| 4/21 |
||
| 4/23 |
||
| 4/28 |
Projects Due | |
| 4/30 |
Course Projects
Half of your grade in this class will be determined by a course project, which may be completed in small groups. Projects that relate synergistically with other ongoing research are encouraged.
- Groups:
Teams for group projects will consist of one, two, or three students. - Timeline:
- February 17: 2-page Project proposals are due
- April 28: Final Project due
- Topic:
The only requirement is that the topic of the project be somehow related to linear logic. Here are some ideas to get your creative juices flowing:- Write a survey paper about some aspect of linear logic: its connections to memory management, concurrency, mu calculus, separation logic, ...
- Implement a linear-logic-based type system
- Implement a theorem prover based on linear-logic
- Implement a Coq library to solve finite multiset goals similar to how the existing MSet package works for finite sets.
- Formalize a substructural logic in Coq. Prove cut elimination.
- Pick a categorical model of linear logic and work out lots of concrete examples using that model.