Local computation in linear logic

This work deals with the exponential fragment of Girard's linear logic without the contraction rule, a logical system which has a natural relation with the direct logic. A new sequent calculus for this logic is presented in order to remove the weakening rule and recover its behavior via a special treatment of the propositional constants, so that the process of cut-elimination can be performed using only ''local'' reductions. Hence a typed calculus, which admits only local rewriting rules, can be introduced in a natural manner. Its main properties - normalizability and confluence - has been investigated; moreover this calculus has been proved to satisfy a Curry-Howard isomorphism with respect to the logical system in question.