Normalization and sub-formula property for Lambek with product and PCMLL -- Partially Commutative Multiplicative Linear Logic

Maxime Amblard, Christian Retoré

This paper establishes the normalisation of natural deduction or lambda calculus formulation of Intuitionistic Non Commutative Logic --- which involves both commutative and non com…