CS 662A: Introduction to Linear Logic

Prerequisites: CS202 for UG students. No prerequisite for PG students

 

Credits: 3-0-0-9 (Equivalent to 2.5 hrs of lectures/week)

 

Course Objective:

Linear Logic was introduced by J. Y. Girard in 1987. This was followed by rapid new development of this field and its applications for a decade or so. Currently concepts and techniques related to these works are used in many areas of logic and semantics of computation. Objective of this course is to cover a set of core topics in linear logic to provide firm background to study more advanced topics.

 

Syllabus:

 

1. Sequent Calculus presentation of propositional linear logic. Cut-Elimination theorem. Undecidability.
2. Connection with computation via Curry-Howard isomorphism. Computational interpretaions.
3. Connection with computation via linear logic programming. Uniform proofs, an example programming language like Lolli.
4. Categorical framework for semantics of linear logic. Games and other models.
5. Proof nets.
6. Depending on availaility of time, basics of some topics like Geometry of interaction, Abstract machines, Bounded linear logic may be taken up.

 

References:

 

1. A. Troelstra: Lecture on Linear Logic. CSLI Stanford publication, 1991. Kindle edition 2015.
2. S. Abramsky: Computational interpretations of Linear Logic. Theoretical Computer Science 111(1&2): 3-57 (1993).
3. S. Abramsky, R. Jagadeesan. New foundations of geometry of interactions. Information and Computation 111(1): 53-119 (1994).
4. J. Y. Girard, P. Ruet, P. Scott, T. Ehrhard (Editors). Linear Logic in Computer Science.  London Mathematical Society Lecture Note Series, 316, 2004.
5. Some other research papers.