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)
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.
- Sequent Calculus presentation of propositional linear logic. Cut-Elimination theorem. Undecidability.
- Connection with computation via Curry-Howard isomorphism. Computational interpretaions.
- Connection with computation via linear logic programming. Uniform proofs, an example programming language like Lolli.
- Categorical framework for semantics of linear logic. Games and other models.
- Proof nets.
- Depending on availaility of time, basics of some topics like Geometry of interaction, Abstract machines, Bounded linear logic may be taken up.
- A. Troelstra: Lecture on Linear Logic. CSLI Stanford publication, 1991. Kindle edition 2015.
- S. Abramsky: Computational interpretations of Linear Logic. Theoretical Computer Science 111(1&2): 3-57 (1993).
- S. Abramsky, R. Jagadeesan. New foundations of geometry of interactions. Information and Computation 111(1): 53-119 (1994).
- J. Y. Girard, P. Ruet, P. Scott, T. Ehrhard (Editors). Linear Logic in Computer Science. London Mathematical Society Lecture Note Series, 316, 2004.
- Some other research papers.