Normalization and interpolation for semi-substructural logics
- LecturerDr. Cheng-Syuan Wan (Tallinn University of Technology)
Host: Liang-Ting Chen - Time2025-11-04 (Tue.) 10:30 ~ 12:30
- Location資訊所新館101演講廳 , Auditorium 101 at IIS new Building
Abstract
In this talk, I will give an introduction to semi-substructural logics from a proof-theoretic perspective, including sequent calculi, normalization, and interpolation.
Semi-substructural logics are motivated from skew monoidal categories. Introduced by Szlachányi in his work on bialgebroids and independently by Altenkirch et al. in their study of relative monads for programming language semantics, these categories relax the associativity and unit laws of traditional monoidal categories from natural isomorphisms to natural transformations with a specific orientation. This relaxation has spurred significant interest in category theory.
Given that monoidal categories are categorical models for linear logics via the Curry-Howard-Lambek correspondence, semi-substructural logics emerge as the logical counterparts of skew monoidal categories and their variants. These logics are situated between non-associative and associative versions of non-commutative intuitionistic linear logic (or the Lambek calculus).
Semi-substructural logics are motivated from skew monoidal categories. Introduced by Szlachányi in his work on bialgebroids and independently by Altenkirch et al. in their study of relative monads for programming language semantics, these categories relax the associativity and unit laws of traditional monoidal categories from natural isomorphisms to natural transformations with a specific orientation. This relaxation has spurred significant interest in category theory.
Given that monoidal categories are categorical models for linear logics via the Curry-Howard-Lambek correspondence, semi-substructural logics emerge as the logical counterparts of skew monoidal categories and their variants. These logics are situated between non-associative and associative versions of non-commutative intuitionistic linear logic (or the Lambek calculus).