Embedded Files
Instructors
Instructors
Structure of the course
Structure of the course
Abstract. Linear logic can be seen in various ways as a substructural type system, as a resource-conscious logic, or as the internal logic of a certain kind of categories. This course is intended to give the students a taste of linear logic, familiarising them with the various bespoke aspects of the subject so that they can read more advanced topics on their own. Basic knowledge of sequent calculus and category theory is assumed. For brushing up on sequent calculus, one might look at the first instructor's notes for an introductory course on Proof Theory at MGS'24. A preliminary draft of the lecture notes are now up. After every exercise session, solutions will be posted.
Abstract. Linear logic can be seen in various ways as a substructural type system, as a resource-conscious logic, or as the internal logic of a certain kind of categories. This course is intended to give the students a taste of linear logic, familiarising them with the various bespoke aspects of the subject so that they can read more advanced topics on their own. Basic knowledge of sequent calculus and category theory is assumed. For brushing up on sequent calculus, one might look at the first instructor's notes for an introductory course on Proof Theory at MGS'24. A preliminary draft of the lecture notes are now up. After every exercise session, solutions will be posted.
Lecture 1 (Abhishek)
Lecture 1 (Abhishek)
Motivation for studying linear logic
Sequent calculus for linear logic and syntactic concerns
(Chapters 1,2)
Lecture 2 (Abhishek)
Lecture 2 (Abhishek)
Focussing -- a proof search strategy
Translating intuitionistic and classical logic into linear logic
(Chapter 3)
Lecture 3 (Charles)
Lecture 3 (Charles)
Relational semantics as denotational semantics where both formulas and proofs are interpreted
Relational semantics as a particular kind of categorical semantics
(Chapter 4)
Lecture 4 (Abhishek)
Lecture 4 (Abhishek)
Proof nets -- a graphical presentation of proofs that simplifies cut elimination
(Chapter 5)
We would appreciate your feedback on this course! Please follow this link and leave us a feedback. It should take less than 5 mins.
We would appreciate your feedback on this course! Please follow this link and leave us a feedback. It should take less than 5 mins.
Google Sites
Report abuse