1 Linear Logic Appeared in SIGACT 1992 Linear Logic

Girard’s claims such as “Linear logic is a resource conscious logic”. Increasingly, computer scientists have recognized linear logic as an expressive and powerful logic, with deep connections to concepts from computer science. The expressive power of linear logic is evidenced by some very natural encodings of computational models such as Petri nets, counter machines, Turing machines, and others. This note presents an intuitive overview of linear logic, some recent theoretical results, and some interesting applications of linear logic to computer science. Other introductions to linear logic may be found in [12, 36]. 2 Linear Logic vs Classical and Intuitionistic Logics Linear logic differs from classical and intuitionistic logic in several fundamental ways. Classical logic may be viewed as if it deals with static propositions about the world where each proposition is either true or false. Because of the static nature of propositions in classical logic, one may “duplicate ” propositions: P implies (P and P). Implicitly we learn that “one P is as good as two”. Also, one may discard propositions: (P and Q) implies P. Here the proposition Q has been “thrown away”. Both of these sentences are valid in classical logi