Local computation in linear logic

✍ Scribed by Ugo Solitro; Silvio Valentini

• Book ID: 102941880
• Publisher: John Wiley and Sons
• Year: 1993
• Tongue: English
• Weight: 613 KB
• Volume: 39
• Category: Article
• ISSN: 0044-3050
• DOI: 10.1002/malq.19930390123

✦ Synopsis

Abstract

This work deals with the exponential fragment of Girard's linear logic ([3]) without the contraction rule, a logical system which has a natural relation with the direct logic ([10], [7]). 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 ([6]) with respect to the logical system in question. MSC: 03B40, 03F05.