A Brief Guide to Linear Logic

andre scedrov^{∗}

Department of Mathematics, University of Pennsylvania Philadelphia, PA 19104-6395, USA

Abstract

An overview of linear logic is given, including an extensive bibliography and a simple example of the close relationship between linear logic and computation.

1 Overview

Linear logic, introduced by Girard [41], is a refinement of classical logic. Linear logic is sometimes described as resource sensitive because it provides an intrinsic and natural accounting of resources. This is indicated by the fact that in linear logic, two assumptions of a formula A are distinguished from a single assumption of A. Informally, on the level of basic intuition, one might say that classical logic is about truth, that intuitionistic logic is about construction of proofs, and that linear logic is about process states, events, or resources, which must be carefully accounted for.

A convenient way to present the syntax of linear logic is by modifying the traditional Gentzen-style sequent calculus axiomatization of classical logic, which may be found in e.g., Girard et al. [49] or in Gallier [38]. The modification may be briefly described in three steps, bearing in mind that assumptions are viewed as resources, and conclusions as requirements to be met by spending the given resources. In this reading the formula A implies A, for instance, means that the resource A is spent to meet the requirement A. This is an axiom in linear logic.

∗andre@cis.upenn.edu. Research partially supported by NSF Grant CCR-91-02753 and by ONR Grant N00014-92-J-1916. This is an updated version of the article that has originally appeared in the Bulletin of the European Association for Theoretical Computer Science vol. 41, June, 1990, pp. 154-165 in the column “Logic in Computer Science”

edited by Yuri Gurevich. This version will appear in a collection of articles published by World Scientific and edited by G. Rozenberg.

The first step in presenting linear logic as a modification of classical logic is to remove two “structural” rules, contraction and weakening, which manipulate the use of assumptions and conclusions in logical deductions. For expository purposes let us concentrate on the treatment of assumptions. The contraction rule states that if a property follows from two assumptions of a formula, then that property can be derived just from a single assumption of that formula. In effect, this means that any assumption, once stated, may then be reused as often as desired. For instance, the formula A implies (A and A) is derivable from contraction. The weakening rule makes it possible to form deductions that have dummy assumptions, i.e., weakening allows us to carry out a deduction without using all of the assumptions. For instance, the formula (A and B) implies A is derivable from weakening. Because contraction and weakening together make it possible to use an assumption as often or as little as desired, these rules are responsible for what one may see in hindsight as a loss of control over resources in classical (and in intuitionistic) logic. This realization is the starting point of linear logic. Removing the rules of contraction and weakening produces a linear system in which each assumption must be used, nay, spent exactly once. In the resulting linear logic, formulas indicate finite resources that cannot necessarily be discarded or duplicated without effort.

The second step in deriving linear logic involves the propositional connectives. Briefly, the removal of structural rules just mentioned leads naturally to two forms of conjunction, one called multiplicative and the other additive, and similarly to two forms of disjunction. A proof of the multiplicative conjunction as a conclusion forbids any sharing between the resources used to establish each conjunct, whereas the additive conjunction requires the sharing of all of the resources. We should mention that unlike this distinction between the two forms of conjunction and disjunction, the quantifier rules remain the same as in classical logic.

The third step in the presentation of linear logic involves adding a kind of modality: a storage or reuse operator, ! . Intuitively, the assumption !A provides unlimited use of the resource A. A computational metaphor that describes the meaning of !A quite well is that “the datum A is stored in the memory and may be referenced an unlimited number of times”. There is also a dual modal operator, ? , which is definable from ! using negation. Intuitively, while !A provides unlimited creation of A, the formula ?B allows the unlimited consumption of B.

Because the basic framework remains linear, unbounded consumption or reuse is allowed “locally”, only at formulas specifically marked with ? or ! , respectively. In effect, the structural rules of contraction and weakening are replaced by the explicit logical rules about the modalities. The resulting logical system is remarkably natural and well-structured, and it brings logical form and content closer together. Linear logic also indicates a relationship between classical logic and intuitionistic logic that is more subtle than the standard negative interpretation, see Girard [45, 46].

Detailed descriptions of linear logic rules may be found in, e.g., [41, 68, 85]. Let us mention that the nonmodal fragment of linear logic was anticipated by a calculus proposed by Lambek [62, 63], motivated by linguistic considerations of syntax of natural languages.

A remarkable result of Lincoln and Winkler [71] shows that there is no simple minded truth table characterization of provability even for the multiplicative fragment of linear logic, unless p = np (see below). In this sense semantics of linear logic is necessarily involved. Basic linear algebra constructions on finite dimensional vector spaces provide a first, naive interpretation of some of the linear logic connectives, much as the basic operations on sets provide an interpretation of the usual logical connectives. For instance, multiplicative conjunction may be interpreted as tensor product of vector spaces and linear negation may be interpreted as the dual vector space. More subtle aspects of linear logic, however, originate in so-called coherence domains [41], which maintain a notion of finite basis and isomorphism with the double dual without imposing isomorphism with the dual. Indeed, an important turning point in the discovery of linear logic was Girard’s insight that in coherence domains, function type A ⇒ B could be decomposed as !A−∘B , where ! is the reuse operator mentioned above, and −∘ is linear implication, which provides the type of functions that “use” their argument exactly once.

Similar phenomena had been previously observed by Blass in certain natural set-theoretic operations on infinite games [23] and by Barr in so-called *- autonomous categories [16]. Both settings, in addition to coherent domains, are now understood to yield mathematical models for linear logic proofs, more precisely, for the relation “ t is a linear logic proof of a formula A ” [24, 84, 17]. Other versions of game semantics are given by Abramsky and Jagadeesan [2] and by Lafont and Streicher [61]. Event spaces, which come about from Pratt’s work in semantics of concurrency, also provide models for certain linear logic proofs [78]. Models investigated by de Paiva [35] are motivated by important proof-theoretic transformations. A mathematical model for the linear logic provability relation is given by phase spaces, discussed by Girard [41] and by Avron [14, 15]. Kripke-style models are investigated by Allwein and Dunn [6].

A mathematical structure underlying linear logic proof reduction and normalization is provided by proof nets, introduced by Girard [41, 42, 47] and studied by Danos and Regnier [34], Blute [25, 26], and others. A significant insight into dynamic, operational semantics of linear logic proof reduction (cut elimination) is provided by geometry of interaction, proposed by Girard [43, 44]; an exposition is in Danos [32]. Geometry of interaction is further investigated in the work of Danos [33], Regnier [79], Malacaria and Regnier [74], Abramsky and Jagadeesan [3], and Gonthier et al. [51, 52] (see below).

Linear logic continues to be a very active field of research. Up-to-date developments are discussed on the electronic forum “Linear”. One subscribes by sending an email message to linear-request@cs.stanford.edu. An introductory description of linear logic is in Lincoln [65]. The first book on linear logic, by Troelstra [85], was published in 1992. It provides a valuable first reference for anyone interested in studying the subject.

2 Computational Aspects

Computer science ramifications of linear logic may be generally divided into two kinds. In what may be broadly called functional programming ramifications (often involving certain aspects of concurrency), computation is seen as term reduction corresponding to proof reduction (cut elimination). On the other hand, in what may be broadly called logic programming ramifications (again, often involving concurrency), computation is expressed by cut free proof search in certain linear logic theories. From the latter perspective, the cut elimination property is used simply to allow one to concentrate on cut free proofs without loss of generality. Certain permutability properties, which yield optimized presentations of cut free proofs play a central role in the proof search paradigm, see Lincoln [72], Andreoli [7].

2.1 Proof Reduction Paradigm

The earliest work in this direction was Lafont’s investigation of a functional programming language implementation in which garbage collection was replaced by explicit duplication operations based on linear logic [59]. Another possible application in functional programming is in optimization of copying in lazy functional programming language implementation (“singlethreadedness”), studied by Guzmán and Hudak [54]. Recent topics involve linear lambda calculus and memory allocation, investigated by Lincoln and Mitchell [66], Chirimar et al. [30], Wadler [86], Mackie [73], and Benton et al. [22].

A strong relationship of the multiplicative fragment of linear logic to Petri nets has been demonstrated by Gehlot and Gunter [53, 40, 39], Asperti et al. [11, 13], Engberg and Winskel [37], Marti-Oliet and Meseguer [75], and Brown and Gurr [27]. Interpretations of linear logic proofs in concurrent paradigms such as the chemical abstract machine or Milner’s π-calculus are given by Abramsky [1] and by Bellin and P.J. Scott [21]. With regard to concurrency, we also note a remarkable similarity between a programming paradigm based on proof nets and developed by Lafont [60] and connection graphs, which were designed by Bawden to model the massively parallel connection machine computations [18].

A modular setting for polynomial time computations can be given in a bounded linear logic, studied by Girard et al. [50]. In this system unlimited reuse is not allowed. Instead, bounded linear logic contains bounded or limited reuse operators. A bounded reuse operator of order n indicates that a datum is stored in the memory and may be referenced at most n times, where variable n is the bound. Proof-rules of the sequent calculus then naturally generate polynomial bounds. Bounded linear logic has polynomial time cut elimination. This system might serve as a basis for a modular calculus of efficient algorithms.

Recent topics include the use of geometry of interaction by Gonthier et al. [51, 52] in a correctness proof for Lamping’s graph reduction. (A companion reference is Asperti [12].) Lamping [64] discovered an optimal graphreduction implementation of the lambda calculus, independently of Girard’s work on geometry of interaction (see above). Gonthier et al. show how the geometry of interaction provides a suitable semantic basis for explaining and improving Lamping’s system. On the other hand, Gonthier et al. show that graphs similar to Lamping’s and related to Lafont’s nets (see above) provide a concrete representation of the geometry of interaction.

2.2 Proof Search Paradigm

Linear logic is also related to computation in another way, namely, computation may be expressed by cut free proof search in certain linear logic theories. The remarkable expressiveness of this computational paradigm is brought to light in a body of research accumulated over the past three years. In a number of papers Andreoli and Pareschi develop a declarative treatment of object communication and concurrent object-oriented computation [8, 9, 7, 10]. A treatment of linear logic programming is given by Hodas and Miller [55]. A role of linear logic in a declarative semantics of SLDNF-resolution is considered by Cerrito [29]. An approach that spans both the proof reduction and the proof search paradigms is proposed by Girard [48].

Recent topics include a treatment of concurrent constraint programming by Saraswat and Lincoln [82] and a closely related treatment of Milner’s π-calculus of communicating processes by Miller [76]. In Miller’s work the agent expressions of the π-calculus are translated into a theory of linear logic in such a way that the π-calculus reductions are identified, step by step, with cut free proof search in the linear logic theory. The nonlogical axioms of the theory resemble Horn clauses except that they may have multiple conclusions. In particular, their heads may be the multiplicative disjunction of atomic formulas. Such multiple conclusion clauses are used to axiomatize communications among agents.

The striking expressiveness of cut free linear logic proof search as a computational paradigm is also indicated by the complexity and undecidability of (provability in) the natural fragments of linear logic. This comes about as a consequence of direct, lockstep simulations of computations on generic machines by cut free proof search in fragments of linear logic, see Section 3 below. The simulations reveal a structural relationship between the natural fragments of linear logic on the one hand and the standard computational complexity classes on the other. Lincoln et al. [68] show that the full propositional (i.e., quantifier free) linear logic is undecidable. However, even the fragment of propositional linear logic that does not allow modalities is unexpectedly expressive. Kanovich [57] shows that the multiplicative fragment is np-complete. Furthermore, in a marked contrast to the standard np-completeness of the satisfiability of propositional formulas in classical logic, in linear logic even the decision problem for constant-only multiplicative propositional formulas is np-complete. This result, obtained by Lincoln and Winkler [71], shows that a simple minded, efficient, truth-table style characterization of provability in the multiplicative fragment of linear logic would imply that p = np. Beyond the multiplicatives, Lincoln et al. [68] show pspace-completeness of the nonmodal propositional fragment (i.e., the multiplicative-additive propositional fragment). Lincoln et al. [70] exhibit a structural embedding of a cut free proof system for implicational propositional intuitionistic logic in the nonmodal propositional linear logic. Lincoln and Scedrov [69] obtain nexptime-hardness of nonmodal linear logic with first order quantifiers and function symbols.

3 Example

This section describes an example of the ability of linear logic to express computational features. A simple computation on an ordinary two counter machine with zero-test instruction is simulated, step by step, by cut free proof search in propositional linear logic. A key insight is that searching for a certain kind of proof of a linear logic formula from finitely many nonlogical axioms that involve only multiplicative conjuction ⊗ and additive disjunction ⊕ corresponds directly to searching for an accepting computation. The product of a successful search is an accepting computation. This example is taken from Lincoln et al. [68, 67].

Suppose the transition relation δ of a standard two counter machine with zero-test consists of the following:

δ_{1} : : = Q_{I} Increment A Q_{2}
δ_{2} : : = Q_{3} Decrement A Q_{F}
δ_{3} : : = Q_{2} Zero-Test B Q_{3}

The machine may perform the following transitions, where an instantaneous description of a two counter machine is given by the triple consisting of Q_{j}, the current state, and the values of counters A and B.

⟨Q_{I}, 0, 0⟩ ⟶^{δ_{1}} ⟨Q_{2}, 1, 0⟩ ⟶^{δ_{3}} ⟨Q_{3}, 1, 0⟩ ⟶^{δ_{2}} ⟨Q_{F} , 0, 0⟩

This computation starts in state Q_{I}, increments the A counter and steps to state Q_{2}. Then it tests the B counter for zero, and moves to Q_{3}, where it then decrements the A counter, moves to Q_{F}, and accepts.

The transition relation δ may be transformed into a transition relation δ′ for an equivalent and-branching two counter machine without zero-test, or briefly acm. The modified relation δ′ (shown on the left below), may then be encoded as a linear logic theory (shown on the right):

Transitions

δ′_{1} : : = Q_{I} Increment A Q_{2}
δ′_{2} : : = Q_{3} Decrement A Q_{F}
δ′_{3} : : = Q_{2} Fork Z_{B}, Q_{3}
δ′_{4} : : = Z_{B} Decrement A Z_{B}
δ′_{5} : : = Z_{B} Fork Q_{F} , Q_{F}

Theory Axioms q_{I} ⊢ (q_{2} ⊗ a) q_{3}, a ⊢ q_{F} q_{2} ⊢ (z_{B} ⊕ q_{3}) z_{B}, a ⊢ z_{B} z_{B} ⊢ (q_{F} ⊕ q_{F})

Notice how the first two transitions (δ_{1} and δ_{2}) of the standard two counter machine are preserved in the translation from δ to δ′. Also, the Zero-Test instruction δ_{3} is encoded as three acm transitions — δ′_{3}, δ′_{4}, and δ′_{5}. The transition δ′_{3} is a fork to a special state Z_{B}, and one other state, Q_{3}. The two extra transitions, δ′_{4} and δ′_{5}, force the computation branch starting in state Z_{B} to verify that counter B is zero. Given the above transitions, the and-branching machine without zero-test may then perform these moves:

\begin{matrix}\{⟨Q_{I}, 0, 0⟩\} ⟶^{δ′_{1}} \{⟨Q_{2}, 1, 0⟩\} ⟶^{δ′_{3}} \{⟨Z_{B}, 1, 0⟩, ⟨Q_{3}, 1, 0⟩\} ⟶^{δ′_{4}} \{⟨Z_{B}, 0, 0⟩, ⟨Q_{3}, 1, 0⟩\} \\ ⟶^{δ′_{5}} \{⟨Q_{F} , 0, 0⟩, ⟨Q_{F} , 0, 0⟩, ⟨Q_{3}, 1, 0⟩\} ⟶^{δ′_{2}} \{⟨Q_{F} , 0, 0⟩, ⟨Q_{F} , 0, 0⟩, ⟨Q_{F} , 0, 0⟩\} \end{matrix}

Note that an instantaneous description of this and-branching machine is a list of triples, and the machine accepts if and only if it is able to reach ⟨Q_{F} , 0, 0⟩ in all branches of its computation. This particular computation starts in state Q_{I}, increments the A counter and steps to state Q_{2}. Then it forks into two separate computations; one which verifies that the B counter is zero, and the other which proceeds to state Q_{3}. The B counter is zero, so the proof of that branch proceeds by decrementing the A counter to zero, and jumping to the final state Q_{F}. The other branch from state Q_{3} simply decrements A and moves to Q_{F}. Thus all branches of the computation terminate in the final state with both counters at zero, resulting in an accepting computation.

The linear logic proof corresponding to this computation is displayed in Figures 1 and 2, and is explained in the following paragraphs. In these proofs, each application of a theory axiom corresponds to one step of acm computation. We represent the values of the acm counters in unary by copies of the formulas a and b. In this example the B counter is always zero, so there are no occurrences of b.

The proof shown in Figure 1 of z_{B}, a ⊢ q_{F} in the above linear logic theory corresponds to the acm verifying that the B counter is zero. Reading the proof bottom up, it begins with a directed cut. The sequent z_{B} ⊢ q_{F} is left as an intermediate step. The next step is to use another directed cut, and after application of the ⊕ L rule, we have two sequents left to prove: q_{F} ⊢ q_{F} and q_{F} ⊢ q_{F}. Both of these correspond to the acm triple ⟨Q_{F} , 0, 0⟩ which is the accepting triple, and are provable by the identity rule. If we had attempted to prove this sequent with some occurrences of b, we would be unable to complete the proof.

\overline{z_{B}, a ⊢ z_{B}}^{δ4^{′}}  \underline{\overline{z_{B} ⊢ (q_{F} ⊕ q_{F})}^{δ5^{′}}  \underline{\overline{q_{F} ⊢ q_{F}}^{I} \overline{q_{F} ⊢ q_{F}}^{I}}_{⊕L} ; (q_{F} ⊕ q_{F}) ⊢ q_{F}}_{Cut} ; z_{B} ⊢ q_{F} Cut
z_{B}, a ⊢ q_{F}

Figure 1: Zero-test proof

The proof shown in Figure 2 of q_{I} ⊢ q_{F} in the same theory demonstrates the remainder of the acm machinery. The lowermost introduction of a theory axiom, Cut, and ⊗ L together correspond to the application of the increment instruction δ′_{1}. That is, the q_{I} has been “traded in” for q_{2} along with a. The application of a directed cut and ⊕ L correspond to the fork instruction, δ′_{3} which requires that both branches of the proof be successful in the same way that and-branching machines require all branches to reach an accepting configuration. The indicated proof of z_{B}, a ⊢ q_{F} appears in Figure 1, and corresponds to the verification that the B counter is zero.

q_{I} ⊢ (q_{2} ⊗ a) δ1^{′}

\overline{q_{2} ⊢ (z_{B} ⊕ q_{3})}^{δ3^{′}}  \underline{⋮ ; z_{B}, a ⊢ q_{F}  \underline{\overline{q_{3}, a ⊢ q_{F}}^{δ2^{′}} \overline{q_{F} ⊢ q_{F}}^{I}}_{Cut} ; q_{3}, a ⊢ q_{F}}_{⊕L} ; (z_{B} ⊕ q_{3}), a ⊢ q_{F} Cut
q_{2}, a ⊢ q_{F}
\overline{(q_{2} ⊗ a) ⊢ q_{F}}^{⊗L} Cut
q_{I} ⊢ q_{F}

Figure 2: Proof corresponding to computation

The application of Cut, theory axiom, and identity correspond to the final decrement instruction of the computation, and complete the proof.

References

[1] S. Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 1992. Special Issue on the 1990 Workshop on Math. Found. Prog. Semantics. To appear.

[2] S. Abramsky and R. Jagadeesan. Games and full completeness for multiplicative linear logic. Manuscript, September 1992. Available using anonymous ftp from the host theory.doc.ic.ac.uk and the file theory/papers/Abramsky/gfc.dvi.

[3] S. Abramsky and R. Jagadeesan. New foundations for the geometry of interaction. In Proc. 7-th Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, pages 211–222. IEEE Computer Society Press, Los Alamitos, California, June 1992.

[4] V.M. Abrusci. Noncommutative intuitionistic linear propositional logic. Zeitschr. f. Math. Logik u. Grundlagen d. Math., 36:297–318, 1990.

[5] V.M. Abrusci. Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic. Journal of Symbolic Logic, 56:1403–1451, 1991.

[6] G. Allwein and J.M. Dunn. Kripke models for linear logic. Manuscript, January 1992.

[7] J.-M. Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 1992. To appear.

[8] J.-M. Andreoli and R. Pareschi. Logic programming with sequent systems: a linear logic approach. In Proc. Workshop on Extensions of Logic Programming, Tuebingen. Lecture Notes in Artificial Intelligence, Springer-Verlag, Berlin, 1990.

[9] J.-M. Andreoli and R. Pareschi. Linear objects: Logical processes with built-in inheritance. New Generation Computing, 9, 1991.

[10] J.-M. Andreoli and R. Pareschi. Associative communication and its optimization via abstract interpretation. Manuscript, August 1992.

[11] A. Asperti. A logic for concurrency. Technical report, Dipartimento di Informatica, Universitá di Pisa, 1987.

[12] A. Asperti. Linear logic, comonads and optimal reductions. Manuscript, December 1991.

[13] A. Asperti, G.-L. Ferrari, and R. Gorrieri. Implicative formulae in the ‘proofs as computations’ analogy. In Proc. 17-th ACM Symp. on Principles of Programming Languages, San Francisco, pages 59–71, January 1990.

[14] A. Avron. The semantics and proof theory of linear logic. Theoretical Computer Science, 57:161–184, 1988.

[15] A. Avron. Some properties of linear logic proved by semantic methods. Manuscript, December 1991.

[16] M. Barr. *-Autonomous Categories, volume 752 of Lecture Notes in Mathematics. Springer-Verlag, Berlin, 1979.

[17] M. Barr. Accessible categories and models of linear logic. Journal Pure Appl. Algebra, 69:219–232, 1990.

[18] A. Bawden. Connection graphs. In Proc. ACM Symp. on Lisp and Functional Programming, pages 258–265, 1986.

[19] G. Bellin. Mechanizing Proof Theory: Resource-Aware Logics and Proof-Transformations to Extract Implicit Information. PhD thesis, Stanford University, 1990.

[20] G. Bellin and J. Ketonen. A decision procedure revisited: Notes on direct logic, linear logic, and its implementation. Theoretical Computer Science, 95:115–142, 1992.

[21] G. Bellin and P.J. Scott. Remarks on the π-Calculus and Linear Logic. Manuscript to be submitted to Proc. MFPS 8, Oxford, 1992.

[22] N. Benton, G. Bierman, V. de Paiva, and J.M.E. Hyland. Term assignment for intuitionistic linear logic. Manuscript, September 1992.

[23] A. Blass. Degrees of indeterminacy of games. Fundamenta Mathematicae, 77:151–166, 1972.

[24] A. Blass. A game semantics for linear logic. Annals Pure Appl. Logic, 56:183–220, 1992. Special Volume dedicated to the memory of John Myhill.

[25] R. Blute. Linear logic, coherence, and dinaturality. Dissertation, University of Pennsylvania, September 1991. Edited version to appear in Theoretical Computer Science.

[26] R. Blute. Proof nets and coherence theorems. In Category Theory and Computer Science, Proceedings 1991. Springer LNCS 530, 1991.

[27] C. Brown and D. Gurr. A categorical linear framework for Petri nets. In Proc. 5-th IEEE Symp. on Logic in Computer Science, Philadelphia, June 1990.

[28] C. Brown and D. Gurr. Relations and noncommutative linear logic. Manuscript, December 1991.

[29] S. Cerrito. A linear semantics for allowed logic programs. In Proc. 5-th IEEE Symp. on Logic in Computer Science, Philadelphia, June 1990.

[30] J. Chirimar, C. Gunter, and J. Riecke. Linear ML. In Proc. ACM Symposium on Lisp and Functional Programming, San Francisco. ACM Press, June 1992.

[31] J. Chirimar and J. Lipton. Provability in TBLL: A decision procedure. In Computer Science Logic, Proceedings 1991, pages 341–356. Springer LNCS 626, 1992.

[32] V Danos. Logique linéaire. une représentation algébrique du calcul. Gaz. Math. (Soc. Math. de France), 41:55–64, 1989.

[33] V. Danos. La Logique Linéaire Appliquée à l’Étude de Divers Processus de Normalisation at Principalement du Lambda-Calcul. Thèse de Doctorat, Université de Paris VII, 1990.

[34] V. Danos and L. Regnier. The structure of multiplicatives. Archive for Mathematical Logic, 28:181–203, 1989.

[35] V.C.V. de Paiva. A dialectica-like model of linear logic. In Category Theory and Computer Science, pages 341–356. Springer LNCS 389, September 1989.

[36] K. Dosen. Nonmodal classical linear predicate logic is a fragment of intuitionistic linear logic. Theoretical Computer Science, 102:207–214, 1992.

[37] U. Engberg and G. Winskel. Petri nets as models of linear logic. In A. Arnold, editor, Proceedings of CAAP ’90. Lecture Notes in Computer Science vol. 431, Springer-Verlag, 1990.

[38] J.H. Gallier. Logic for computer science. Harper & Row Publishers, New York, 1986.

[39] V. Gehlot. A proof-theoretic approach to semantics of concurrency. Dissertation, University of Pennsylvania, 1991.

[40] V. Gehlot and C.A. Gunter. Normal process representatives. In Proc. 5th IEEE Symp. on Logic in Computer Science, Philadelphia, June 1990.

[41] J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

[42] J.-Y. Girard. Multiplicatives. Rendiconti del Seminario Matematico dell’ Universitá e Politecnico Torino, Special Issue on Logic and Computer Science, pages 11–33, 1987.

[43] J.-Y. Girard. Geometry of interaction I: Interpretation of system F. In Logic Colloquium ’88, Amsterdam, 1989. North-Holland.

[44] J.-Y. Girard. Geometry of interaction II: Deadlock-free algorithms. In: Springer LNCS 417, 1990.

[45] J.-Y. Girard. A new constructive logic: classical logic. Mathematical Structures in Computer Science, 1:255–296, 1991.

[46] J.-Y. Girard. On the unity of logic. Manuscript, 1991.

[47] J.-Y. Girard. Quantifiers in linear logic II. Prépublications Paris 7 Logique, No. 19, January 1991.

[48] J.-Y. Girard. A fixpoint theorem in linear logic. Announcement on ‘Linear’ electronic forum , February 1992.

[49] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1989.

[50] J.-Y. Girard, A. Scedrov, and P.J. Scott. Bounded linear logic: A modular approach to polynomial time computability. Theoretical Computer Science, 97:1–66, 1992.

[51] G. Gonthier, M. Abadi, and J.-J. Levy. The geometry of optimal lambda reduction. In Proc. 19-th Annual ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico. ACM Press, New York, NY, January 1992.

[52] G. Gonthier, M. Abadi, and J.-J. Levy. Linear logic without boxes. In Proc. 7-th Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, pages 223–234. IEEE Computer Society Press, Los Alamitos, California, June 1992.

[53] C.A. Gunter and V. Gehlot. Nets as tensor theories. In G. De Michelis, editor, Proc. 10-th International Conference on Application and Theory of Petri Nets, Bonn, pages 174–191, 1989.

[54] J.C. Guzman and P. Hudak. Single-threaded polymorphic lambda calculus. In Proc. 5-th IEEE Symp. on Logic in Computer Science, Philadelphia, June 1990.

[55] J.S. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. In Proc. 6-th Annual IEEE Symposium on Logic in Computer Science, Amsterdam, pages 32–42. IEEE Computer Society Press, Los Alamitos, California, July 1991. Full paper to appear in Information and Computation. Draft available using anonymous ftp from host ftp.cis.upenn.edu and the file pub/papers/miller/ic92.dvi.Z.

[56] B. Jacobs. Semantics of weakening and contraction. Manuscript, May 1992.

[57] M. Kanovich. Horn programming in linear logic is NP-complete. In Proc. 7-th Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, pages 200–210. IEEE Computer Society Press, Los Alamitos, California, June 1992.

[58] J. Ketonen and R. Weyhrauch. A decidable fragment of predicate calculus. Theoretical Computer Science, 32, 1984.

[59] Y. Lafont. The linear abstract machine. Theoretical Computer Science, 59:157–180, 1988.

[60] Y. Lafont. Interaction nets. In Proc. 17-th ACM Symp. on Principles of Programming Languages, San Francisco, pages 95–108, January 1990.

[61] Y. Lafont and T. Streicher. Game semantics for linear logic. In Proc. 6th Annual IEEE Symposium on Logic in Computer Science, Amsterdam, pages 43–50. IEEE Computer Society Press, Los Alamitos, California, July 1991.

[62] J. Lambek. The mathematics of sentence structure. Amer. Math. Monthly, 65:154–169, 1958.

[63] J. Lambek. Multicategories revisited. In Categories in Computer Science and Logic, pages 217–239. Contemporary Math., vol. 92, American Math. Soc., Providence, RI, 1989.

[64] J. Lamping. An algorithm for optimal lambda calculus reduction. In Proc. 17-th Annual ACM Symposium on Principles of Programming Languages, San Francisco, pages 16–30. ACM Press, New York, NY, January 1990.

[65] P. Lincoln. Linear logic. ACM SIGACT Notices, 23(2):29–37, Spring 1992.

[66] P. Lincoln and J. Mitchell. Operational aspects of linear lambda calculus. In Proc. 7-th Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, pages 235–246. IEEE Computer Society Press, Los Alamitos, California, June 1992.

[67] P. Lincoln, J. Mitchell, A. Scedrov, and N. Shankar. Decision problems for propositional linear logic. In Proc. 31st IEEE Symp. on Foundations of Computer Science, pages 662–671, 1990.

[68] P. Lincoln, J. Mitchell, A. Scedrov, and N. Shankar. Decision problems for propositional linear logic. Annals Pure Appl. Logic, 56:239–311, 1992. Special Volume dedicated to the memory of John Myhill.

[69] P. Lincoln and A. Scedrov. First order linear logic without modalities is NEXPTIME-hard. Manuscript, September 1992. Available using anonymous ftp from host ftp.cis.upenn.edu and the file pub/papers/scedrov/mall1.dvi.

[70] P. Lincoln, A. Scedrov, and N. Shankar. Linearizing intuitionistic implication. In Proc. 6-th Annual IEEE Symposium on Logic in Computer Science, Amsterdam, pages 51–62. IEEE Computer Society Press, Los Alamitos, California, July 1991. Full paper to appear in Annals of Pure and Applied Logic. Draft available using anonymous ftp from host ftp.cis.upenn.edu and the file pub/papers/scedrov/lss91.dvi.

[71] P. Lincoln and T. Winkler. Constant-Only Multiplicative Linear Logic is NP-Complete. Manuscript, September 1992. Available using anonymous ftp from host ftp.csl.sri.com and the file pub/lincoln/comult-npc.dvi.

[72] P.D. Lincoln. Computational Aspects of Linear Logic. PhD thesis, Stanford University, 1992.

[73] I. Mackie. Lilac - a functional programming language based on linear logic. Master’s Thesis, Imperial College, London, 1991.

[74] P. Malacaria and L. Regnier. Some results on the interpretation of λcalculus in operator algebras. In Proc. 6-th Annual IEEE Symposium on Logic in Computer Science, Amsterdam, pages 63–72. IEEE Computer Society Press, Los Alamitos, California, July 1991.

[75] N. Marti-Oliet and J. Meseguer. From Petri nets to linear logic. In: Springer LNCS 389, ed. by D.H. Pitt et al., 1989. 313-340.

[76] D. Miller. The π-calculus as a theory in linear logic: Preliminary results. Technical Report MS-CIS-92-48, Computer Science Department, University of Pennsylvania, June 1992. Submitted. Available using anonymous ftp from host ftp.cis.upenn.edu and the file pub/papers/miller/pic.dvi.Z.

[77] H. Ono. Phase structures and quantales — a semantical study of logics without structural rules. Manuscript, 1991.

[78] V.R. Pratt. Event spaces and their linear logic. In AMAST ’91: Algebraic Methodology and Software Technology, Iowa City, 1991, Workshops in Computing, pages 1–23. Springer-Verlag, 1992.

[79] L. Regnier. λ-calcul et Réseaux. Thèse de Doctorat, Université de Paris VII, 1992.

[80] D. Roorda. Resource logics: proof-theoretical investigations. Dissertation, University of Amsterdam, September 1991.

[81] K.I. Rosenthal. Girard quantaloids. Mathematical Structures in Computer Science, 2:93–108, 1992.

[82] V. Saraswat and P. Lincoln. Higher-order, linear, concurrent constraint programming. Manuscript, August 1992.

[83] H. Schellinx. Some syntactical observations on linear logic. Journal of Logic and Computation, 1:537–559, 1991.

[84] R.A.G. Seely. Linear logic, *-autonomous categories, and cofree coalgebras. In Categories in Computer Science and Logic, pages 371–382. Contemporary Math., vol. 92, American Math. Soc., Providence, RI, 1989.

[85] A.S. Troelstra. Lectures on Linear Logic. CSLI Lecture Notes No. 29. Center for the Study of Language and Information, Stanford University, 1992.

[86] P. Wadler. There’s no substitute for linear logic. Manuscript, December 1991.

[87] D.N. Yetter. Quantales and (noncommutative) linear logic. Journal of Symbolic Logic, 55:41–64, 1990.