ALC Seminar | Speaker: Cheng-Syuan Wan (Tallinn University of Technology, Estónia)

Title: Proof Theory of Skew Logics

Abstract: Skew 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. 

Given that monoidal categories are the base of categorical models for linear logics via the Curry-Howard-Lambek correspondence, skew 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).

In this talk, I will give an introduction to skew logics from a proof-theoretic perspective, including sequent calculi, normalization, and interpolation.