A typed calculus based on a fragment of linear logic

AbstractLinear Logic, we concisely write LL, has been introduced recently by Jean Yves Girard in Theoretical Computer Science 50 (1987). Born from the semantics of second order lambda calculus, LL is more expressive than traditional logic (both classical and intuitionistic). Due to the absence of structural rules and to a particular treatment of negation, which is denoted by ⊥, proofs in LL do not have a “directional character”. The constructive meaning of a proof of A→B is a function mapping all proofs of A into proofs of B; in LL A⊸B has a similar meaning, but B⊥⊸A⊥ represents the same formula and has the same proofs: so one of such proofs can map a proof of A into one of B as well as a proof of B⊥ into one of A⊥. In this paper we are interested in the multiplicative second order subsystem LL∗ of linear logic; we introduce a calculus (called v-calculus) whose terms are canonical representations of proofs. The aim of the calculus is to give a better comprehension of the computational aspects of the process of cut-elimination. We prove that the v-calculus obeys strong normalization and the Church-Rosser properties