Tutorial on Linear Logic
Anne S. Troelstra · 1993
Abstract In this tutorial we present a very elementary introduction to linear logic, consisting of a description of the system, a sketch of cut-elimination, a discussion of the relationship with intuitionistic logic (embedding theorems), a sketch of completeness for algebraic semantics, and some remarks on the computational interpretation. From a technical point of view linear logic appears as a refinement of ordinary logic; in a sequential formulation in Gentzen-style this is obtained by omitting the rules of contraction and weakening (thinning); afterwards weakening and contraction are reintroduced for specific formulas with help of special operators storage (!) and costorag (?).