Strong normalizability of typed lambda-calculi for substructural logics (Q1001367)

Standard \(\lambda\)-calculus has, as its set of types, the theorems of intuitionistic implicational logic \(H_\to\). The theorems of weaker implicational logics, and some logics with \(\to\) and \(\wedge\) have been shown to be the types of subsystems or extensions of the \(\lambda\)-calculus. This paper concerns \(\lambda\)-calculi, previously introduced by the authors, whose theorems are the types of a large number of substructural logics over the \(\{ /, \backslash , \ast \}\)-fragment \(L\) of the full Lambek Logic and the \(\{ /, \backslash , \ast , \sim \}\)-fragment \(C\) of the constructive sequential logic. The authors, in a single proof, prove strong normalisation for all the \(\lambda\)-calculi at once!