Intuitionistic Sequent-Style Calculus with Explicit Structural Rules

Abstract : In this paper we extend the Curry-Howard correspondence to intuitionistic sequent calculus with explicit weakening and contraction. We study a system derived from /\-Gtz of Espirito Santo by adding explicit operators for weakening and contraction, which we call l/\-Gtz. This system contains only linear terms. For the proposed calculus we introduce the type assignment system with simple types. The presented system has a natural diagrammatic representation, which is used for proving the subject reduction property. We prove the strong normalisation property by embedding l/\-Gtz into the simply typed /\lxr calculus of Kesner and Lengrand.