Linear Logic

First published Wed Sep 6, 2006; substantive revision Sat Sep 16, 2023

Linear logic is a refinement of classical and intuitionistic logic.Instead of emphasizingtruth, as in classical logic, orproof, as in intuitionistic logic, linear logic emphasizesthe role of formulas asresources. To achieve this focus,linear logic does not allow the usual structural rules of contractionand weakening to apply to all formulas but only those formulas markedwith certain modals. Linear logic contains a fully involutive negationwhile maintaining a strong constructive interpretation. Linear logicalso provides new insights into the nature of proofs in both classicaland intuitionistic logic. Given its focus on resources, linear logichas found many applications in Computer Science.

1. Introduction

1.1 A bit of history

Linear logic was introduced by Jean-Yves Girard in his seminal work (Girard 1987). While the origin of the discovery of this new logic comes from asemantical analysis of the models of System F (or polymorphic$\lambda$-calculus), one can see the whole system of linear logic asa bold attempt to reconcile the beauty and symmetry of classical logicafforded by De Morgan's dualities with the quest for constructive proofsthat had led to intuitionistic logic.

Indeed, one could present a fragment of linear logic, known asmultiplicative additive linear logic (MALL), as the outcomeof two simple observations.

In the sequent calculus presentation of classical logic, the rulesfor the connectives “and” and“or”, as well as the Cut rule and the rule forimplication may be presented equivalently in an additive form (thecontext of the premises are the same) or a multiplicative form (thecontext of the premises are different). These two presentations areequivalent, in classical logic, because of the availability of a fewso-called “structural” rules, namely, contraction andweakening.
Gentzen's use of the sequent calculus to capture proofs for bothclassical and intuitionistic logics demonstrated that non-constructiveproofs made use of one or the other of these structural rules in theconclusion (succedent) of sequents.

So, if we want to eliminate the non-constructive proofs withoutdestroying the symmetry of the sequent calculus, as is done inintuitionistic logic, we can try to eliminate the contraction andweakening rules instead. In doing so, we are left with two differentversions of each connective: an additive version and a multiplicativeversion of conjunction and of disjunction. These different versions ofthe same connecitve are now no longer equivalent. These newconnectives are & (“with”, additiveand),$\oplus$ (“plus”, additiveor), $\otimes$(“tensor”, multiplicativeand) and $\lpar$(“par”, multiplicativeor).

This duplication of the connectives actually leads to a much clearerunderstanding of the conflict between classical and intuitionisticlogic. For example, the law of excluded middle ($A$ornot-$A$) is considered valid in the classical world and absurd inthe intuitionistic one. But in linear logic, this law has tworeadings: the additive version $(A \oplus \neg A)$ is not provableand corresponds to the intuitionistic reading of disjunction; themultiplicative version $(A \lpar \neg A)$ is trivially provable andsimply corresponds to the tautology $(A$implies $A)$that is perfectly acceptable in intuitionistic logic too.

Also, the disjunction property, essential in constructivism, is easilyestablished for the additive disjunction.

We find then inside this richer logic a way to represent both theneeds of intuitionism and the elegance of classical logic: negation isinvolutive, sequents are symmetric, and connectives areinter-definable. Contrast these properties with those ofintuitionistic logic, where negation is not involutive, sequents arenot symmetric, and connectives $\neg, \wedge, \vee, \Rightarrow$ are all not inter-definable.

Notice that once one has eliminated the contraction andweakening rules, formulas no longer behave as truth values. Indeed, ifwe compose a proof of $A \Rightarrow B$ and a proof of $A$ withoutthese structural rules, we consume them to get a proof of $B$: thatis, $A \Rightarrow B$ and $A$ are no longer available after thecomposition. Linear logic formulas behave more likeresources that can only be used in restricted ways.

To recover the full expressive power of intuitionistic and classicallogic, it is then necessary to add to the MALL fragment two dualmodalities, which are usually calledexponentials in thelinear logic literature. In particular, the “of-course”exponential $\bang$ permits contraction and weakening to be appliedto the formula $\bang B$ in the left-hand sequent context while the“why-not” exponential $\quest$ permits contraction andweakening to be applied to the formula $\quest B$ on the right-handsequent context. This leads to the full propositional linear logic andto a very nice connection with computer science.

Notice that besides MALL, there are two other widely used fragments ofLinear Logic: Multiplicative Linear Logic (MLL), which is MALL withoutthe additive connectives; and Multiplicative Exponential Linear Logic(MELL), which is Linear Logic without the additive connectives.

Gentzen's sequent calculus proof system for intuitionistic logic wasthe result of restricting his sequent calculus for classical logic sothat all sequents contained at most one formula on the right-hand sideof sequents (Gentzen 1935). Such a single-conclusion restriction can also be explored in thecontext of linear logic. Various researchers have consideredintuitionistic variants of MLL, MALL, and MELL: for example, IMLL (Lamarche 1996), IMALL (Lincolnet al. 1993), and IMELL (Dal Lago and Laurent 2008). Schellinx (1991) provided some general conservativity results of classical linear logic over the corresponding intuitionistic variants: see also(Troelstra 1992).

Prior to the introduction of linear logic in 1987, various researchershad been working on various kinds of substructural logic in which notall of Gentzen’s structural rules (contraction, weakening, andexchange) are accepted. Lambek studied a sequent calculus proofsystems in which none of these structural rules were permitted (Lambek 1958). Other examples of such logics are relevant logic (in which weakeningis not accepted) (Anderson & Belnap 1975,Andersonet al. 1992,Avron 1988,Read 1988). and affine logic (in which contraction is not accepted) (Grishin 1981).

1.2 Linear logic and computer science

The computer science exploitation of intuitionistic and constructive logic began when people saw the possibility of reading$A \Rightarrow B$ as‘if you give me an $A$, I will give you a $B$’, whichis a significant departure from the classical reading‘$A$ isfalse or $B$ is true’.

Linear logic provides a further twist in the interpretation of theimplication ‘$A \Rightarrow B$’: now it can be read as‘give meas many $A$'s as I might need and I willgive youone $B$’. The notion ofcopy whichis so central to the idea of computation is now wired into the logic.This new viewpoint opens up new possibilities, including:

new formulas expressing refined operational propertieslike ‘give me $A$ once and I will give you $B$’.Applications here range from refined logic programming where theability of linear logic to represent states is put to use (Hodas & Miller, 1994), to the analysis of classical logic and computational interpretationsthereof (Abramsky 1993), to the specification of exception mechanisms in programming languages (Miller, 1996), and to linearity analysis (Wadler, 1991).
new rules expressing constraints on the use of copiesresulting in a fragment of linear logic for polytime computations tomention only the most spectacular application (Baillot & Terui, 2004,Baillot 2015).
new ways of representing proofs (Abramsky & Jagadeesan, 1994,Girard 1987).

2. Proof Systems

The core propositional connectives of linear logic are divided intoadditive and multiplicative connectives. The classical conjunction andits identity, $\wedge$ and $\top$, split into the additive$\amp$ (with) and $\top$ (top) and the multiplicative $\otimes$(tensor) and 1 (one). Similarly, the classical disjunction and itsidentity, $\vee$ and $\bot$, split into the additive $\oplus$(oplus) and 0 (zero) and the multiplicative $\lpar$ (par) and$\bot$ (bottom). Negation is generally treated in one of two ways inpresentations a linear logic. Negation can be viewed as a primitivepropositional connective with no restrictions on its occurrenceswithin formulas. Since De Morgan dualities exist between negation andall propositional connectives, exponentials, and quantifiers, it isalso possible to treat negation as a special symbol that only occursapplied to atomic formulas. Implications are also commonly introducedinto linear logic via definitions: the linear implication $B \limpC$ can be defined as $B^{\bot} \lpar C$, while the intuitionisticimplication $B \Rightarrow C$ can be defined as $\bang B \limp C$.The operators $\bang$ and $\quest$ are variously called modals orexponentials. The term “exponential” is particularlyappropriate since, following the usual relationship betweenexponentiation, addition, and multiplication, linear logic supportsthe equivalences $\bang (B \amp C) \equiv (\bang B \otimes \bang C)$and $\quest(B \oplus C) \equiv (\quest B \lpar \quest C)$, as wellas the 0-ary versions of these equivalences, namely, $(\bang\top\equiv 1)$ and $(\quest 0 \equiv \bot)$. Here, we use the binaryequivalence $B \equiv C$ to mean that the formula $(B \limp C)\amp(C \limp B)$ is derivable in linear logic.

2.1 Sequent calculus

A two-sided sequent calculus for linear logic is presented in thefigure below. Notice here that negation is treated as if it were anyother logic connective: that is, its occurrences in formulas are notrestricted and there are introduction rules on the left and right fornegation. The left and right side of sequents are multiset offormulas: thus, the order of formulas in these contexts does notmatter but their multiplicity does matter.

Identity Rules \[\frac{}{B \vdash B}\ \textit{init} \qquad\frac {\Delta_1 \vdash B,\Gamma_1 \qquad \Delta_2,B \vdash \Gamma_2} {\Delta_1,\Delta_2 \vdash \Gamma_1,\Gamma_2}\ \textit{cut}\]

Negation Rules \[\frac{\Delta \vdash B,\Gamma}{\Delta,B^{\perp} \vdash \Gamma}\ (\cdot)^{\perp} L \qquad\frac{\Delta,B \vdash \Gamma}{\Delta \vdash B^{\perp},\Gamma}\ (\cdot)^{\perp} R\]

Multiplicative Rules \[\frac{\Delta \vdash \Gamma}{\Delta,\one \vdash \Gamma}\ \one L \qquad \frac{}{\vdash \one}\ \one R\] \[\frac{}{\bot \vdash}\ \bot L \qquad \frac{\Delta \vdash \Gamma}{\Delta \vdash \bot,\Gamma}\ \bot R\]\[\frac{\Delta, B_1,B_2 \vdash \Gamma}{\Delta, B_1\ot B_2 \vdash \Gamma}\ \ot L \qquad \frac{\Delta_1 \vdash B_1,\Gamma_1 \qquad \Delta_2 \vdash B_2,\Gamma_2} {\Delta_1, \Delta_2 \vdash B_1\ot B_2,\Gamma_{1},\Gamma_{2}}\ \ot R\] \[\frac{\Delta_1,B_1 \vdash \Gamma_1 \qquad \Delta_2, B_2 \vdash \Gamma_2} {\Delta_1,\Delta_2, B_1\lpar B_2 \vdash \Gamma_1,\Gamma_2}\ \lpar L \qquad \frac{\Delta \vdash B_1, B_2,\Gamma}{\Delta \vdash B_1\lpar B_2, \Gamma}\ \lpar R\]

Additive Rules \[\frac{}{\Delta,\zero \vdash \Gamma}\ \zero L \qquad \frac{}{\Delta \vdash \top,\Gamma}\ \top R\] \[\frac{\Delta, B_i \vdash \Gamma} {\Delta, B_1\amp B_2 \vdash \Gamma}\ {\amp}L\ (i=1,2) \qquad \frac{\Delta \vdash B_1,\Gamma \qquad \Delta \vdash B_2,\Gamma} {\Delta \vdash B_1\amp B_2,\Gamma}\ {\amp}R\] \[\frac{\Delta,B_1 \vdash \Gamma \qquad \Delta,B_2 \vdash \Gamma} {\Delta,B_1\oplus B_2 \vdash \Gamma}\ {\oplus}L \qquad \frac{\Delta \vdash B_i,\Gamma} {\Delta \vdash B_1\oplus B_2,\Gamma}\ {\oplus}R\ (i=1,2)\]

Quantifier Rules \[\frac{\Delta, B[t/x] \vdash \Gamma}{\Delta,\forall x.B \vdash \Gamma}\ \forall L \qquad \frac{\Delta \vdash B[y/x],\Gamma}{\Delta \vdash \forall x.B,\Gamma}\ \forall R\] \[\frac{\Delta \vdash B[t/x],\Gamma}{\Delta \vdash \exists x.B,\Gamma}\ \exists R \qquad \frac{\Delta,B[y/x] \vdash \Gamma}{\Delta,\exists x.B \vdash \Gamma}\ \exists L,\]

Exponential Rules \[\frac{\Delta \vdash \Gamma}{\Delta, \bang B \vdash \Gamma}\ \bang W \quad \frac{\Delta, \bang B, \bang B \vdash \Gamma}{\Delta, \bang B \vdash \Gamma}\ \bang C \quad \frac{\Delta,B \vdash \Gamma}{\Delta, \bang B \vdash \Gamma}\ \bang D \quad \frac{\bang\Delta \vdash B,\quest\Gamma}{\bang\Delta \vdash \bang B,\quest\Gamma}\ \bang R\] \[\frac{\Delta \vdash \Gamma}{\Delta \vdash \quest B,\Gamma}\ \quest W \quad \frac{\Delta \vdash \quest B, \quest B,\Gamma}{\Delta \vdash \quest B,\Gamma}\ \quest C \quad \frac{\Delta \vdash B,\Gamma}{\Delta \vdash \quest B,\Gamma}\ \quest D \quad \frac{\bang\Delta,B \vdash \quest\Gamma}{\bang\Delta,\quest B \vdash \quest\Gamma}\ \quest L\]

Notice that the rules of weakening and contraction are available onlyfor formulas marked with the exponential $\bang$ on the left or$\quest$ on the right of the sequent. The $\quest$R and $\bang$Lrules are often called “dereliction” rules. The $\quest$L and $\bang$R rules are often called“promotion” rules andare similar to the sequent calculus rules used in the treatment ofS4 modal logic (Ono 1998). The usualproviso for the $\forall$-right and $\exists$-left introductionrules is assumed; in particular, the variable $y$ must not be freein the formulas of the lower sequent of those inference rules.Quantification here is assumed to be first-order. Girard presented a higher-order version of linear logic in his1987 paper.

The cut rule can be eliminated and completeness is still maintained.Dually, theinit rule can also be eliminated as well exceptfor the occurrences ofinit involving atomic formulas.

2.2 Focused proofs

An important normal form theorem for the structure of cut-free proofswas provided by Andreoli (1992). He classified a non-atomic formula asasynchronous if itstop-level logical connective is $\top$, &, $\bot , \lpar$,$\quest$, or $\forall$ orsynchronous if its top-levellogical connective is $0, \oplus , 1, \otimes$, $\bang$, or$\exists$.

When viewing proof search as a computational model, we consider how inference rules can transform a sequent as itsconclusion intopremises. As a result, we can see formulas in a sequent as being “agents” that may actindependently or in concert with others in their environment. Here, the actions of such agents are determined by reading the introductionrule for them bottom-up. If an asynchronous formula occurs on theright of a sequent, it can evolve without affecting provability andwithout interacting with its context, i.e., the correspondingintroduction rule is invertible. For example, the agent $(B \lparC)$ becomes (by applying the $\lpar$-right introduction rule) thetwo agents $B$ and $C$ (now working in parallel). Similarly, theagent $(B \amp C)$ yields (by applying the &-right introductionrule) two different identical worlds (sequents) except that $B$ isin one of these worlds and $C$ is in the other.

On the other hand, if we view a synchronous formula as an agent whoseevolution is determined by reading the corresponding right-introduction rule from the bottom up,then it is possible for a provable sequent to evolve to a non-provablesequent (for example, by applying the $\oplus$ right-introductionrule). Also, the instances of such inference rules depend on detailsof the context of the formula. For example, the success of the 1-rightintroduction rule requires that the surrounding context is empty andthe success of the $\otimes$-right introduction rule depends on howthe agent’s surrounding context is divided into two contexts.Thus, the evolution of such agents depends on“synchronizing” with other parts of the context.

Now consider a one-sided sequent calculus presentation of linear logicwhere the only introduction rules are right-introduction rules. Giventhe above classification of connectives, it is possible to show thatproof search can be structured into the following phases without lossof completeness. Theasynchronous phase occurs if there is anasynchronous formula present in the sequent. In this phase,right-introduction rules are applied (bottom-up) in any order until there are nofurther asynchronous formulas. In thesynchronous phase somesynchronous formula is selected and becomes the “focus” ofthis phase: that is, right-introduction rules are applied (bottom-up) to it and toany synchronous subformula that it might generate.

The following figure presents the focusing proof system for linearlogic. Notice that the two phases are represented by different arrows:the up-arrow denotes the asynchronous phase and the down-arrow denotesthe synchronous phase. Also, sequents are divided into threezones (where the zones are separated by either a semicolon oran up or down-arrow). In particular, to the left of the up-arrow anddown-arrow are the two zones. The zone written as $\Psi$ denotes aset of formulas that can be used any number of times in the proof ofthat sequent. The zone written as $\Delta$ denotes a multiset offormulas. The zone to the right of anup-arrow is also a multiset of formulas while the zone to the right ofa down-arrow is a single formula. It is possible to impose anarbitrary order on the formulas to the right of the up-arrow since theintroduction of asynchronous formulas can be done in any order. Atomsare given polarity and in the figure below, $A$ stands for positiveatoms and the negation of $A$ stands for negative atoms. Proofsbuilt by these inference rules are calledfocused proofs. Thecompleteness of focused proofs for linear logic is proved inAndreoli 1992.

Asynchronous Phase \[\frac{\Up{\Psi}{\Delta}{L}}{\Up{\Psi}{\Delta}{\bot,L}}\ [\bot] \qquad\frac{\Up{\Psi,F}{\Delta}{L}} {\Up{\Psi}{\Delta}{\quest F,L}}\ [\quest]\] \[\frac{} {\Up{\Psi}{\Delta}{\top,L}}\ [\top] \qquad\frac{\Up{\Psi}{\Delta}{F[y/x],L}} {\Up{\Psi}{\Delta}{\forall x.F,L}}\ [\forall]\]\[\frac{\Up{\Psi}{\Delta}{F_1,F_2,L}} {\Up{\Psi}{\Delta}{F_1\lpar F_2,L}}\ [\lpar] \qquad\frac{\Up{\Psi}{\Delta}{F_1,L}\quad \Up{\Psi}{\Delta}{F_2,L}} {\Up{\Psi}{\Delta}{F_1\amp F_2,L}}\ [\amp]\] \[\frac{\Up{\Psi}{\Delta,F}{L}}{\Up{\Psi}{\Delta}{F,L}} \ [R\Uparrow]\ \text{provided that $F$ is not asynchronous}\]

Synchronous Phase \[\frac{}{\Down{\Psi}{\cdot}{\one}}\ [\one] \qquad \frac{\Down{\Psi}{\Delta_1}{F_1}\quad \Down{\Psi}{\Delta_2}{F_2}} {\Down{\Psi}{\Delta_1,\Delta_2}{F_1\ot F_2}} \ [\ot]\qquad\frac{\Up{\Psi}{\cdot}{F}}{\Down{\Psi}{\cdot}{\bang F}} \ [\bang]\] \[\frac{\Down{\Psi}{\Delta}{F_i}}{\Down{\Psi}{\Delta}{F_1\oplus F_2}} \ [\oplus_i] \qquad\frac{\Down{\Psi}{\Delta}{F[t/x]}} {\Down{\Psi}{\Delta}{\exists x.F}} \ [\exists]\]\[\frac{\Up{\Psi}{\Delta}{F}}{\Down{\Psi}{\Delta}{F}} \ [R\Downarrow]\ \text{provided that $F$ is either asynchronous or an atom} \]

Identity and Decide Rules \[\frac{}{\Down{\Psi}{A}{A^{\perp}}} \ [I_1]\qquad \frac{}{\Down{\Psi,A}{\cdot}{A^{\perp}}} \ [I_2]\ \text{where } A \text{ is an atom}\] \[\frac{\Down{\Psi}{\Delta}{F}}{\Up{\Psi}{\Delta,F}{\cdot}} \ [D_1]\qquad \frac{\Down{\Psi}{\Delta}{F}}{\Up{\Psi,F}{\Delta}{\cdot}} \ [D_2]\ \text{where } F \text{ is a positive formula}\]

Focused proof systems have also been designed for classical andintuitionistic logics (Danoset al. 1997;Laurentet al. 2005;Liang & Miller 2009).

2.3 Proof nets

Proofs presented using a sequent calculus contain a lot of detail thatsometimes is uninteresting: consider for example how manyuninterestingly different ways there are to form a proof of $\vdash\Gamma , (A_1\lpar A_2), \ldots ,(A_{n-1}\lpar A_n)$ from aderivation of $\vdash \Gamma , A_1, A_2 , \ldots ,A_n$. Thisunpleasant fact derives from the sequential nature of proofs in asequent calculus: if we want to apply a set $S$ of $n$ rules todifferent parts of a sequent, we cannot apply them in one step, evenif they do not interfere with each other! We mustsequentialize them, i.e., choose a linear order on $S$ andapply the rules in $n$ steps, according to this order.

A natural question arises: “Is there a representation of proofsthat abstracts from such uninteresting details?”. A similarquestion is answered positively in the case of intuitionistic sequentcalculus by means of what is known asnatural deduction, thathas, via the Curry-Howard correspondence (Howard 1980),a strong connection with thecomputational device known as $\lambda$-calculus.

For linear logic, this succinct representation of proofs is given byproof nets, graph-like structures that enjoy particularlygood properties for the MLL fragment of the logic. The first steptowards this representation is to convert all the sequent calculussystem, using the involutivity of negation, into a one-sided system,where sequents are of the form $\vdash \Gamma$. As a consequence,the number of rules is reduced since we have no left-introductionrules, but we keep the same expressive power, as provability stays thesame.

To each sequent calculus proof in MLL, one can inductively associate aproof net with the sameconclusions as follows:

To a proof reduced to the axiom rule, we associate anaxiomlink.
For a proof obtained by applying the cut rule to two proofs, wefirst inductively build the proof nets associated to those two proofs,and then we combine them using acut link.
For a proof obtained by applying the tensor rule to two proofs, wefirst inductively build the proof nets associated to those two proofs,and then we combine them using atensor link.
For a proof obtained by applying the par rule to a proof, firstinductively build the proof net associated to that proof, and then weadd a “par link”.

All this can be properly formalized using hypergraphs (formulas arenodes and “links” are oriented hyperedges with hypothesesand conclusions), and we can formally define as a proof net ahypergraph inductively built out of a sequent calculus derivation ofMLL. Notice that there are quite a lot of hypergraphs that are notproof nets.

Now if you look at the proof net built from the derivations of$\vdash \Gamma , (A_1\lpar A_2), \ldots ,(A_{n-1}\lpar A_n)$obtained from $\vdash \Gamma , A_1, A_2 , \ldots ,A_n$, you will seethat all trace of the order of application of the rules hasdisappeared. In a sense, the proof nets are an equivalence class ofsequent calculus derivations with respect to the derivation order ofrules whose application commute.

Suppose that somebody now comes to you with a huge hypergraph builtwith axiom, cut, par and tensor links, claiming that it is actuallya representation of a proof.How can you verify that it is actually a representation of aproof, and not just a random structure?

Performing thiscorrectness check is a challenge that amountsto rebuilding a sequential construction history for your structure,corresponding to a derivation in sequent calculus, and seems at firsta very complex problem. The first correctness criterion for MLL proofnets, called the “long trip criterion”, and present inGirard’s original paper, is exponential, as well as the ACC(Acyclic connected) criterion of Danos and Regnier (1989) found later on. Nevertheless, there exists a much more efficientcriterion, known as Contractibility, due to Danos and Regnier, thathas more recently been reformulated as the following elegant graphparsing criterion by Guerrini, Martini and Masini: a hypergraph is aproof net if and only if it reduces to the singleton node“net” via the following graph reduction rules

Graph Parsing for MLL proof net recognition

Performing this check naively can take quadratic time (eachapplication of a rule may require an entire lookup of the graph tofind the redex, and we need to perform as many steps as there arehyperlinks in the graph). Linear time algorithms have been give byGuerrini (2011) and by Murawski and Ong (2006).

Another style of correctness criterion for MLL proof nets is given byRetoré(2003) in which a quadratic algorithm is given for MLL.

On proof nets, one can perform cut elimination in a particularly cleanway, because of their parallel nature, cuts can be eliminated locally viatwo simplification rules:

Axiom move:
Multiplicative move:

These are actually computation rules over proof nets, and thecorrectness criteria allow to verify easily that any such rulepreserves correctness, and as a consequence, the reduction of a proofnet still comes from a sequent calculus proof of the same sequent.

Hence, cut elimination in MLL proof nets can be performed in lineartime and gives a simple, elegant cut-elimination result for all ofMLL.

The proof nets approach can be extended to larger subsets of linearlogic, but then it is less clear how to obtain the same elegantresults as for MLL: the original system proposed inGirard 1987 works for MELL, for example, by associating to the four exponentialrules the following hypergraph constructions:

Contraction
Weakening
Dereliction
Promotion, that introduces the notion of “box”, asequentialization mark around a piece of a proof net materialized inthe pictures of the graphs by the rectangle drawn around the proof netof conclusions $A$ and $\quest\Gamma$.

While these constructions and the associated graph reductions bearstriking similarity with $\lambda$-calculus with explicitsubstitutions, as first remarked by Di Cosmo & Kesner (1997), they are too similar to the corresponding sequent calculus rules. Theparallelization effect so elegant for MLL does not properly carry onhere, and the graph reduction rules involve boxes and are notlocal.

To recover a satisfactory system, many proposals have been made,starting from the one by Danos & Regnier (1995) but we want to mention here the very elegant approach by Guerrini,Martini and Masini (Guerriniet al. 2003), that neatly shows the connection between two level proof systems formodal logic, proper proof nets for MELL, and optimal reduction in the$\lambda$-calculus.

A recent paper by Heijltjes and Houston(2016) has shown that there can be no satisfactory notion of proof nets forMLL if units are also allowed.

It is possible to provide a canonical treatment of additiveconnectives, even with first-order quantification(Heijltjeset al. 2019). Proof nets for formulas containing both multiplicative and additiveconnectives have various technical presentations, none of whichappears canonical and satisfactory. Their treatment in proof-net-likeproof systems is currently a topic of active research. In particular,see(Hughes and van Glabbeek 2005) and(Hughes and Heijltjes 2016).

3. Semantics

Approaching the semantics of linear logic is usually done along twodifferent paths. First, there are various semantic structuresavailable that can be used to map formulas to denotations in suchstructures. That approach can be used to establish soundness andcompleteness for various fragments of linear logic. A more novelsemantic approach to linear logic involves giving semantics to proofsdirectly. We describe briefly these two approaches and provide somelinks to the literature.

3.1 Semantics of provability

One approach to attempting a sound and complete semantics forfragments of linear logic associates to a formula the set of allcontexts that can be used to prove that formula. Of course, such acollection may need to be more abstract and to be given variousclosure properties. Thephase semantics of Girard (1987) provides one such semantics: some uses of such semantics have beenmade in computer science to provide counterexamples and as a tool thatcan help establish that a given concurrent system cannot evolve intoanother with certain properties (Fageset al. 2001).Phase semantics have also been used to give semantic proofs of cut eliminationfor both first-order and higher-order versions of linear logic (Okada 1999). Similarly, Kripke-style semantics have been provided inAllwein & Dunn 1993 andHodas & Miller 1994. Quantales, which are certain kind of partially ordered algebraic structures,have also been used to provide semantic models for parts oflinear logic early on (Yetter 1990).

3.2 Semantics of proofs

In the formulas-as-types analogy which is so popular and fruitful intheoretical computer science, a logical system is put incorrespondence with a typed computational device (like typed$\lambda$-calculus), by associating to each proof of that formula aprogram having that formula as a type. For example, a proof of thetautology $A \Rightarrow A$ corresponds to the programfun$(x:A).x:A\rightarrow A$, the identity function onobjects of type $A$. This is why, in constructive logical systems(such as intuitionistic logic and arithmetic), and in linear logic, somuch importance is attached to proofs, to the point that building andstudying models of proofs gets so much more attention than buildingand studying models of provability: we are not satisfied to know thata formula is provable, we really want to know thecomputationalcontent of its proof.

Many models of linear logic proofs have been proposed; we considerthat, to date, the simplest and most intuitive construction is the onebased on the so-called “relational semantics” or“Kripke-style semantics”, where formulas are interpretedas multisets, one-sided sequents are interpreted as tuples ofmultisets, and proofs are interpreted as relations over theinterpretation of sequents (Tortora de Falco 2003,Ehrhard 2012,Melliès 2018). If one wants to give a purelyset-theoretic semantics, without resorting to multisets, it ispossible to do it by means of coherence spaces, sets equipped with aspecial coherence relation, as originally shown by inGirard 1987. There are interesting category theoretical models of linear logic,such as the *-autonomous categories (Barr 1991) and hypercoherences (Ehrhard 1993).

Another approach to the semantics of proofs is given by Girard’sGeometry of Interaction, that allows us to obtain a fullyalgebraic characterization of proofs. To each proof net, one canassociate a partial permutation matrix $\sigma$ corresponding to thecut links, and a proper matrix $M$ corresponding expressions builtout of a certain dynamic algebra, that describe the possible pathsinside the proof net. It is then possible to fully describe the proofnet via theexecution formula

\[\mathrm{EX}(\sigma ,M) = (1-\sigma^2) \left(\sum_i M(\sigma M)\right) (1-\sigma^2)\]

which, in the MLL case, is an invariant of the normalization process.Some nice connection to results coming from data-flow theory has beenshown in some early work of Abramsky & Jagadeesan (1994).

The area of semantics that has developed around so-calledgamesemantics deserves special attention. The strong connectionbetween games and linear logic was pointed out quite early by A. Blass (1992). In fact, there are two different traditions to connecting logic togames. In the tradition ofdialog games dating back toLorenzen, one player attempts to prove a formula while a second playerattempts to refute it. It is possible to provide MALL with such adialog game that is completely symmetric for both the prover and therefuter (Delandeet al. 2010). In another tradition, formulas are interpreted as games, logicalconnectives as game constructors, and proofs as strategies thatdescribe how a player reacts to opponent moves. By imposing differentrestrictions on the rules of the game, one can actually provide aprecise semantics (technically, a fully abstract model) for variousfeatures of actual programming languages, hence the huge interest inthis area over the past years. See, for example,Abramsky & Jagadeesan 1994,Abramsky & Melliès 1999, andHyland & Ong 2000.

4. Complexity

For any given logic, it is useful to know whether or not there is aneffective procedure to determine, for each sentence in the logic, ifit is provable or not. Adecidable logic—i.e., one forwhich there is an effective procedure for provability—is oftendescribed by itscomplexity class, which characterizes howdifficult it is to perform the decision procedure. Extensive researchwork has been dedicated to the study of the complexity anddecidability issues for several fragments of propositional linearlogic. It is known that

MLL provability is NP-complete (Kanovich 1992) and
MALL provability is PSPACE-complete (Lincolnet al. 1992).

Here, NP and PSPACE are complexity classes such that NP$\subseteq$ PSPACE. Surprisingly, for thosethat may forget that the novelty in linear logic lies in the wayformulas are managed without the structural rules of contraction andweakening, these results stay the same even if we focus on thefragments of the logics where only the constants, and no propositionalvariables, are allowed (Lincoln & Winkler 1994). Indeed, it is possible to encode arbitrary formulasinto constant-only formulas preserving provability.

MELL is a surprisingly expressive logic. For example, the reachabilityproblem in Petri nets can be encoded into MELL(Gunter & Gehlot 1989) and that problem is equivalent to the reachability problem of vectoraddition systems with states (VASS)(Reutenauer 1989). Furthermore, the decidability problem of MELL is equivalent to thereachability problem for branching VASS(de Grooteet al. 2004) and the latter is known to have a non-elementary lower bound(Lazic and Schmitz 2015). Thus, if MELL turns out to be decidable, it will be at least TOWER-hard(Lazic and Schmitz 2015). A proof of the decidability of MELL has been given by Bimbó(2015) but a gap in that proof has been reported by Straßburger(2019).

Proofs of the undecidability of propositional linear logic werepublished in the early 1990s (Lincolnetal. 1992,Lincoln 1995).Kanovich (2016) showed that thisundecidability result holds for a greatly reduced fragment ofpropositional linear logic. and a machine checked proof of undecidabilityhas been published in (Forster& Larchey-Wendling, 2019). However, a proofof decidability of propositional linear logic has also been publishedby Bimbó & Dunn in (2022), who alsoclaim to have found mistakes in the above-mentioned papers.

Linear logic with the unrestricted weakening rule added (also known aslinear affine logic) is decidable (Kopylov 1995) and exponential space hard (Urquhart 2000).

A good overview of complexity results surrounding linear logic can befound inLincoln 1995.

5. Computer science impact

When intuitionistic logic was first proposed early in the lastcentury, it was presented as a challenge to the way traditionalmathematicians were supposed to do business. Uses of the excludedmiddle and of proof-by-contradiction were considered suspect andproblematic, particularly in the presence of infinity. Asintuitionistic logic concerns were developed into constructivemathematics, new constructive approaches have arisen to topics such astopology, algebra, and analysis. Given that linear logic encompassesthe dynamics of proof (algorithm) and resources, its primary impacthas been not in traditional mathematics but in computer science.Before overviewing the nature of that impact, we outline the variousways in which logic more generally is used in computer science.

Logic plays different roles in the specification of computations. Wecan identify the following broad different approaches and note whichroles have felt influences from linear logic.

In thecomputation-as-model approach, computations areencoded as mathematical structures and consist of such items as nodes,transitions, and states. Logic is used externally to makestatementsabout those structures. That is, computations areused as models for logical expressions. Intensional operators, such asthe modals of temporal and dynamic logics or the triples of Hoarelogic, are often employed to express propositions about the change instate. This use of logic to represent and reason about computation isprobably the most broadly successful use of logic forrepresenting computation. This role for logic has felt littleinfluence from linear logic.

In thecomputation-as-deduction approach, pieces oflogic’s syntax (such as formulas, terms, types, and proofs) areused directly as elements of the specified computation. In this morerarefied setting, there are two rather different approaches to howcomputation is modeled, called theproof normalizationapproach and theproof search approach.

We outline below the significant impacts that linear logic has had onboth of these different settings.

5.1 Proof normalization

Theproof normalization approach views the state of acomputation as a proof term and the process of computing asnormalization (known alternatively as $\beta$-reduction orcut-elimination). Functional programming can be explained usingproof-normalization as its theoretical basis (Martin-Löf 1982) and has been used to justify the design of new functional programminglanguages, e.g.,Abramsky 1993. Linear logic provides this approach to computational specificationwith new types, new declarative means for statically understanding howresources may be used in a computation, and provided an appealingmeans for formalizing the duality between a function and theenvironment that supplies it with arguments.

Another area where linear logic has been a powerful theoreticalinstrument is that ofoptimal reduction. The problem ofbuilding efficient (optimal) interpreters for the$\lambda$-calculus, that stayed open for quite a long time after itsoriginal definition by J.J. Lévy, was solved for the first timeinLamping 1990, via a sophisticated sharing graph implementation involving a quiteimpressive amount of rules. Using ideas and intuition from linearlogic, many authors reconstructed Lamping’s solution,simplifying it and leading to a rich theory connected to that of theGeometry of Interaction. For further reading, a good reference isAsperti & Guerrini 1998.

The refinement of intuitionistic logic provided by linear logic andthe dualities of linear logic provided a setting in which one couldview a function and its environment as similar entities that interactdually. For example, a function with the type $A \limp B$ can bemodeled as a process that consumes a value of type $A$ from itsenvironment and transforms it into a value of type $B$. In linearlogic, this implication is equivalent to its contrapositive form: thetype $B^{\bot} \limp A^{\bot}$ can lead to interpreting the samefunction as a process that transforms a demand for a value of type$B$ into a demand for a value of type $A$ (notice that this doesnot happen with functions of intuitionistic type since, for example,input argument may be vacuous) (Curien 2003). The recent successes of using game semantics to model functionalcomputation are similarly related to the dual treatment of functionand environment (Abramsky and Jagadeesan 1994,Hyland & Ong 2000).

Finally, we mention that in the area of encoding computation as proofnormalization, linear logic has been used to provide a type-baseddescription of polytime recursive functions. For example, M. Hofmann (2003) introduced a $\lambda$-calculus with modal and linear types thatextended the function algebra ofBellantoni & Cook 1992 to higher types. Types based on linear logic have also been usedwithin functional programs: seeGuzman & Hudak 1990 andWadler 1991.

5.2 Proof search

Theproof search approach views the state of a computation asa sequent (a structured collection of formulas) and the process ofcomputing as the process of searching for a proof of a sequent: thechanges that take place in sequents capture the dynamics ofcomputation. With this view of computation, we generally readinference rules bottom up, i.e., as a transformation of theirconclusion into their premise(s). Logic programming can be explainedusing proof search as its theoretical basis, and linear logic providesthis approach to computational specification with new combinators forbuilding logic programs, new means to capture rich dynamics, and newdeclarative approaches to specifying concurrent computations. (SeeMiller 2004 for an overview of linear logic programming languages.)

The completeness of focusing proof system can be used to provide adeclarative explanation of part of the operational semantics of logicprogramming within linear logic. Consider, for example, the subset$L$ of formulas of linear logic that are built from only theconnectives $\top$, &, $\limp , \Rightarrow$, and $\forall$.(Notice that if one adds $\bot$ to this list, it is possible toencode all connectives of linear logic.) It is possible to see thatcut-free proof search in $L$ can be defined into to phases. Given asequent $\Gamma$; $\Delta \vdash G$, where $\Gamma$ is aset of formulas (which can be contracted and weakened), $\Delta$ ismultiset of formulas (which cannot be contracted nor weakened), and$G$ (the “goal” formula) is a single formula (all from$L)$, then proof search proceeds as follows.

If $G$ is non-atomic, then only a right introduction rule can beused to conclude this sequent. Given this set of connectives, theright rules are invertible and thisgoal-reduction phasecorresponds exactly to the asynchronous phase of focused proofs.
If $G$ is atomic, then proof search proceeds bydeciding on a single formula from a left-hand context.
Once a formula is chosen for thefocus, allleft-introduction rules are applied to only that formula and anypositive subformulas that arise. Thisbackchaining phasecorresponds to the asynchronous phase of focused proofconstruction.

Formally, these various phases can be described using the followinginference rules. Here, a new sequent arrow is introduced: this arrowis labeled with the formula that is the result of a left-introductionrule. Notice that the rule for left-introduction of $\limp$ requiressplitting the $\Delta$ context into two parts $\Delta_1,\Delta_2$(when reading the rule bottom up). There are, of course, $2^n$ suchsplittings if that context has $n \ge 0$ distinct formulas. Thesyntactic variable $A$ in these inference rules ranges over atomicformulas.

Goal Reduction Phase \[\frac{} {\Gamma;\Delta \vdash \top}\ \top R \qquad\frac{\Gamma;\Delta \vdash B \qquad \Gamma;\Delta \vdash C} {\Gamma;\Delta \vdash B \amp C}\ {\amp}R\] \[\frac{\Gamma;\Delta, B \vdash C} {\Gamma;\Delta \vdash B \limp C}\ \limp R \qquad\frac{\Gamma,B ;\Delta \vdash C} {\Gamma;\Delta \vdash B \Rightarrow C}\ {\Rightarrow}R \qquad\frac{\Gamma;\Delta \vdash B[y/x]} {\Gamma;\Delta \vdash \forall x. B}\ \forall R\]

Backchaining Phase \[\frac{\Gamma;\Delta \lvdash{D_1} A} {\Gamma;\Delta \lvdash{D_1\amp D_2}\, A} \ {\amp}L \qquad\frac{\Gamma;\Delta \lvdash{D_2} A} {\Gamma;\Delta \lvdash{D_1\amp D_2} A}\ {\amp}L \qquad\frac{\Gamma;\Delta \lvdash{D[t/x]} A} {\Gamma;\Delta \lvdash{\forall_{\tau}x.D} A}\ \forall L\] \[\frac{\Gamma;\Delta_1 \vdash G \quad \Gamma;\Delta_2 \lvdash{D} A} {\Gamma;\Delta_1,\Delta_2 \lvdash{G\limp D} A} \ {\limp}L \qquad\frac{\Gamma;\cdot \vdash G \quad \Gamma;\Delta \lvdash{D} A} {\Gamma;\Delta \lvdash{G\Rightarrow D} A}\ {\Rightarrow}L\]

Identity and Decide Rules \[\frac{\Gamma,D;\Delta \lvdash{D} A} {\Gamma,D;\Delta \vdash A}\ \textit{decide}{!} \qquad\frac{\Gamma;\Delta \lvdash{D} A} {\Gamma;\Delta,D \vdash A}\ \textit{decide} \qquad\frac{} {\Gamma;\cdot \lvdash{A} A}\ \textit{init}\]

Linear logic restricted to $L$ can be viewed as a linear logicprogramming language. As a consequence, it can serve as aspecification language for computational systems, a role that is alsooccupied by, say, Petri nets, process calculi, $\lambda$-calculus,etc. Given that linear logic has a proof theory and various kinds ofsemantics, broad avenues of reasoning about computations specified in$L$ are provided by the meta-theory of linear logic.

Given that the sequent calculus for linear logic uses multisets offormulas, proof search can directly encodemultisetrewriting. Since many computations can naturally be seen asmultiset rewriting, it has been possible to make numerous connectionsbetween linear logic and Petri nets (Gunter & Gehlot 1989), process calculi (Andreoli & Pareschi 1991,Kobayashiet al. 1999,Miller 1996), and security protocols (Cervesatoet al. 1999,Miller 2003).

6. Variations

6.1 Different treatments of modality

If one uses traditional sequent calculus presentations, the exponentials are notcanonical in the following sense: if you introduce another copy ofexponentials, say $\bang'$ and $\quest'$, with the same rules asthe original ones, there is no way to prove that $\bang$ isequivalent to $\bang'$, and $\quest$ to $\quest'$, while for theother connectives this is easily established. Various applications ofnon-canonical exponentials can be found in (Danos et. al., 1993;Nigam & Miller, 2009). Although the decidability of MELL is currently beingdebated (Bimbó 2015,Straßburger 2019), extending MLL with three pairs of $\bang$ and$\quest$ yields a logic that is undecidable(Chaudhuri 2018). Martini and Masini1995 describe a “2-sequent” proof system in which theexponentials are canonical.

The fact that cut-elimination can make proofs in classical andintuitionistic logic grow to enormous size can be analyzed in terms ofthe application of the contraction rule in those proof systems. Ifproof systems introduce restrictions on contraction, it is possible todesign new logics and proof systems for which cut-elimination has amuch-reduced complexity. For example,elementary linear logic(ELL) is obtained by replacing the $\bang$ and $\quest$introduction by a single rule introducing $\bang$ and $\quest$ atthe same time. As a consequence, ELL can encode all and only theKalmar elementary functions (computable in time bounded by a tower ofexponentials of fixed height) (Girard 1998,Baillot 2015). Still, other variations on the inference rules for theexponentials have been studied. For example,light linearlogic (Girard 1998) andsoft linear logic (Lafont 2004) both characterize functions computable in polynomial time: see also (Baillot & Terui 2004).

6.2 Non-commutative linear logic

While linear logic rejects the universal application of the twostructural rules of weakening and contraction, it allows theunrestricted use of the structural rule calledexchange. Asequent calculus that does not universally employ the exchange rulehas sequents whose left and right contexts are lists: the order offormulas within context becomes an expressive element of the logic. Inthis case, the multiplicative disjunction and conjunction can becomenon-commutative.

One of the first logics that rejects all three structural rules of thesequent calculus was given inLambek 1958. While this logic containstwo implications, it contains neither a negation nor any exponentials. Various papers haveproposed extending linear logic to include non-commutative featuresand, at present, no proposal seems canonical. For a sampling ofnon-commutative linear logics, seeYetter 1990,Abrusci 1991,Retoré 1997,Abrusci & Ruet 1999, andGuglielmi & Straßburger 2001.

6.3 Treatment of unbounded behavior

While the MALL logic is an expressive and novel logic, it is alsodecidable and, thus, not capable of capturing the unbounded behaviorsfound in, say, iteration and recursion. As described above,the addition of the exponentials ! and ? enriches MALL to full linearlogic and to a setting where unbounded behaviors can be captured. Asecond approach to extending MALL to capture unbounded behaviorsinvolves the addition of the least and greatest fixed point operatorsas logical connectives directly into MALL. In order to properlycharacterize fixed points as being either the least or the greatest,it is necessary for the inference rules for fixed points to be“higher-order” in the sense that they involve invariants.Such an extension to MALL (also with first-order quantification andterm equality) has been developed by Baelde (Baelde & Miller, 2007;Baelde 2012) and has been used to provide a proof-theoreticfoundation for model checking (Heath & Miller 2018).

Bibliography

Abramsky, S., 1993, “Computational interpretations of linearlogic”,Theoretical Computer Science, 111:3–57.
Abramsky, S., and Jagadeesan, R., 1994, “New Foundations for the Geometryof Interaction”,Information and Computation, 111(1):53–119.
Abramsky, S., and Melliès, Paul-André, 1999, “ConcurrentGames and Full Completeness”,14th Annual Symposium on Logicin Computer Science, Trento: IEEE Computer Society Press., pp.431–442.
Abrusci, V. M., 1991, “Phase semantics and sequent calculus for purenon-commutative classical linear propositional logic”,Journal of Symbolic Logic, 56(4): 1403–1451.
Abrusci, V.M., and Ruet, P., 1999, “Non-Commutative Logic I: TheMultiplicative Fragment”,Annals of Pure and AppliedLogic, 101(1): 29–64.
Allwein, G. and Dunn, J.M., 1993, “Kripke Models for LinearLogic”,Journal of Symbolic Logic, 58(2):514–545.
Anderson, A. R. and Belnap, N. D., 1975,Entailment: The Logic of Relevance and Necessity (Volume I), Nuel D. Belnap & J. Michael Dunn (eds.), Princeton, N.J.: Princeton University Press.
Anderson, A. R., Belnap, N. D., andDunn, J. M., 1975,Entailment: The Logic of Relevance andNecessity (Volume II), Princeton, N.J.: Princeton UniversityPress.
Andreoli, J.-M., 1992, “Logic programming with focusing proofs in linearlogic”,Journal of Logic and Computation, 2(3):297–347.
Andreoli, J.-M. and Pareschi, R., 1991, “Linear objects: Logicalprocesses with built-in inheritance”,New GenerationComputing, 9(3–4): 445–473.
Asperti, A., and Guerrini, S., 1998, “The Optimal Implementation ofFunctional Programming Languages”, Cambridge Univ. Press.
Avron, A., 1988, “The Semantics and Proof Theory of LinearLogic”,Theoretical Computer Science, 57:161–184.
Baelde, D., 2012, “Least and greatest fixed points in linearlogic”, ACM Transactions on Computational Logic, 13(1).doi:10.1145/2071368.2071370
Baelde, D. and Miller, D., 2007, “Least and greatest fixed points inlinear logic”,Logic for Programming, ArtificialIntelligence, and Reasoning (Lecture Notes in Computer Science:Volume 4790), edited by N. Dershowitz and A. Voronkov, pp.92–106.
Baillot, P., 2015, “On the expressivity of elementary linear logic:Characterizing Ptime and an exponential time hierarchy”,Information and Computation, 241: 3–31.
Baillot, P., and Terui, K., 2004, “Light Types for Polynomial TimeComputation in Lambda-Calculus”,Proceedings of theNineteenth Annual IEEE Symposium on Logic in Computer Science,Turku, Finland, IEEE Computer Society Press, pp. 266–275.
Barr, M., 1991, “*-Autonomous categories and linear logic”,Mathemathical Structures in Computer Science, 1(2):159–178.
Bellantoni, S. and Cook, S., 1992, “A New Recursion-TheoreticCharacterization of the Polytime Functions”,ComputationalComplexity, 2: 97–110.
Bimbó, K., 2015, “Thedecidability of the intensional fragment of classical linearlogic”,Theoretical Computer Science, 597(13):1–17.
Bimbó, K. and J. M. Dunn, 2022,“Modalities in lattice-R”, inRelevance Logics andother Tools for Reasoning. Essays in Honor of J. Michael Dunn,London: College Publications, pp. 89–127.
Blass, A., 1992, “A game semantics for linear logic”,Annalsof Pure and Applied Logic, 56: 183–220.
Cervesato, I., Durgin, N., Lincoln, P., Mitchell, J., and Scedrov, A., 1999,“A meta-notation for protocol analysis”, in R. Gorrieri(ed.),Proceedings of the 12th IEEE Computer Security FoundationsWorkshop—CSFW 1999, Los Alamitos, CA: IEEE Computer SocietyPress, pp. 55–69.
Chaudhuri, K., 2018, “Encoding additives using multiplicatives andsubexponentials”,Mathematical Structures in ComputerScience, 28(5): 651–666.
Curien, P.-L., 2003, “Symmetry and interactivity in programming”,Bulletin of Symbolic Logic, 9(2): 169–180.
Dal Lago, U., and Laurent, O., 2008,“Quantitative Game Semantics for LinearLogic”,Computer Science Logic (Lecture Notes inComputer Science: Volume 5213), Michael Kaminski and Simone Martini(eds.), Berlin: Springer, pp. 230–245.
Danos, V., Joinet, J.-P., and Schellinx, H., 1993, “The Structure ofExponentials: Uncovering the Dynamics of Linear Logic Proofs”,pp. 159–171, inKurt Gödel Colloquium (LectureNotes in Computer Science, Volume 713), edited by G. Gottlob, A.Leitsch, and D. Mundici, Berlin: Springer.
–––, 1997, “A New Deconstructive Logic: Linear Logic”,Journal of Symbolic Logic, 62(3): 755–807.
Danos, V. and Regnier, L., 1989, “The Structure ofMultiplicatives”,Archive of Mathematical Logic,Springer, 28:181–203.
–––, 1995, “Proof-nets and Hilbert space”, in J.-Y. Girard, Y.Lafont, and L. Regnier (eds.),Advances in Linear Logic,Cambridge: Cambridge University Press, pp. 307–328.
de Groote, P., Guillaume, B., and Salvati, S., 2004, “Vectoraddition tree automata”, inProceedings of the 19th IEEESymposium on Logic in Computer Science (LICS 2004), 14–17July 2004, Turku, Finland, pp. 64–73.
Delande, O., Miller, D., and Saurin, A., 2010, “Proof and refutation inMALL as a game”,Annals of Pure and Applied Logic,161(5): 654–672.
Di Cosmo, R., and Kesner, D., 1997, “Strong normalization ofexplicit substitutions via cut elimination in proof nets”,(extended abstract) inProceedings of the Twelfth Annual IEEESymposium on Logic in Computer Science, Los Alamitos, CA: IEEEComputer Society Press, pp. 35–46.
Ehrhard, T., 1993, “Hypercoherences: A Strongly Stable Model of LinearLogic”,Mathematical Structures in Computer Science,3(4): 365–385.
–––, 2012,“The Scott model of linear logic is the extensional collapse of its relational model”,Theoretical Computer Science, 13(6):20–45.
Fages, F., Ruet, P., and Soliman, S., 2001, “Linear ConcurrentConstraint Programming: Operational and Phase Semantics”,Information and Computation, 165(1): 14–41.
Forster, Y. and D. Larchey-Wendling,2019, “Certified undecidability of intuitionistic linear logicvia binary stack machines and Minsky machines”,Proceedingsof the 8th ACM SIGPLAN International Conference on Certified Programsand Proofs (CPP’19), New York: Association of ComputingMachinery, pp. 104–117. doi:10.1145/3293880.3294096
Gentzen, G., 1935, “Investigationsinto Logical Deduction”, in M. E. Szabo (ed.),TheCollected Papers of Gerhard Gentzen, Amsterdam: North-Hollandpp. 68–131.
Girard, J.-Y., 1987, “Linear logic”,Theoretical ComputerScience, 50: 1–102.
–––, 1998, “Light Linear Logic”,Information andComputation, 143(2):175–204.
Grishin, V. N., 1981, “Predicate and set-theoretic calculi based onlogic without contraction rules,” (Russian). Izvestiya AkademiiNauk SSSR Seriya Matematicheskaya 45(1): 47–68. 239. Math. USSRIzv., 18, no.1, Moscow.
Guerrini, S., 2011, “A linear algorithm for MLL proof net correctness andsequentialization”,Theoretical Computer Science, 412:1958–1978.
Guerrini, S., Martini, S., and Masini, A., 2003, “Coherence for sharingproof-nets”,Theoretical Computer Science, 294(3):379–409.
Guglielmi, A., and Straßburger, L., 2001, “Non-commutativity andMELL in the Calculus of Structures”,Computer ScienceLogic (Lecture Notes in Computer Science, Volume 2142), Berlin:Springer Verlag, pp. 54–68.
Gunter, C. A., and Gehlot, V., 1989, “Nets as Tensor Theories”,in G. De Michelis (ed.),Proceedings of the Tenth InternationalConference on Application and Theory of Petri Nets (Lecture Notesin Computer Science: Volume 616), Bonn: Springer-Verlag, pp.174–191.
Guzman, J.C. and Hudak, P., 1990, “Single-threaded polymorphic lambdacalculus”, inProceedings of the Fifth IEEE Symposium onLogic in Computer Science, Philadelphia: IEEE Computer SocietyPress.
Heath, Q. and Miller, D., 2018, “A proof theory for modelchecking”,Journal of Automated Deduction,doi:10.1007/s10817-018-9475-3.
Heijltjes, W. and Houston, R., 2016, “Proof equivalence in MLL isPSPACE-complete”,Logical Methods in Computer Science12(1).
Heijltjes, W. B., Hughes, D. J. D., and Straßburger, L., 2018,“Proof nets for first-order additive linear logic”,4th International Conference on Formal Structures for Computationand Deduction, (FSCD 2019: Volume 131), Dagstuhl: Leibniz-Zentrumfür Informatik, pp. 22:1–22:22.
Hodas, J., and Miller, D., 1994, “Logic programming in a fragment ofintuitionistic linear logic”,Information andComputation, 110(2): 327–365.
Hofmann, M., 2003, “Linear types and non-size increasing polynomial timecomputation”,Information and Computation, 183(1):57–85.
Howard, W.A., 1980, “The formulae-as-type notion of construction,1969”, in J.P. Seldin and R. Hindley (eds.),To H. B. Curry:Essays in Combinatory Logic, Lambda Calculus, and Formalism, NewYork: Academic Press, pp. 479–490.
Hughes, D.J.D. and van Glabbeek, R., 2005, “Proof Nets for Unit-FreeMultiplicative-Additive Linear Logic”,ACM Transactions onComputational Logic, 6: 784–842.
Hughes, D.J.D. and Heijltjes, W. B., 2016, “Conflict nets: efficientlocally canonical mall proof nets”,31st Annual ACM/IEEESymposium on Logic in Computer Science (LICS), 2016.
Hyland, J.M.E., and Ong, C.-H.L., 2000, “On Full Abstraction for PCF:I. Models, observables and the full abstraction problem, II. Dialoguegames and innocent strategies, III. A fully abstract and universalgame model”,Information and Computation, 163:285–408.
Kanovich, M.I., 1992, “Horn Programming in Linear Logic isNP-Complete”, inProceedings of the Seventh Annual Symposiumon Logic in Computer Science, Santa Cruz, IEEE Computer SocietyPress, pp. 200–210.
–––,2016, “The undecidability theorem for theHorn-like fragment of linear logic(Revisited)”,Mathematical Structures inComputer Science, 26: 719–744.
Kobayashi, N., Shimizu, T., and Yonezawa, A., 1999, “Distributedconcurrent linear logic programming”,Theoretical ComputerScience, 227(1–2): 185–220.
Kopylov, A. P., 1995, “Decidability of Linear Affine Logic”,Symposium on Logic in Computer Science (LICS’95), IEEE ComputerSociety Press, pp. 496–505.
Lafont, Y., 2004, “Soft linear logic and polynomial time”,Theoretical Computer Science, 318(1–2):163–180.
Lamarche, F., 1996, “FromProof Nets to Games: extended abstract”, inLinear Logic 96Tokyo Meeting,Electronic Notes in Theoretical ComputerScience, 3: 107–119.
Lambek, J., 1958, “The mathematics of sentence structure”,American Mathematical Monthly, 65: 154–169.
Lamping, J., 1990, “An algorithm for optimal lambda-calculusreductions”. 17th Annual Symposium on Principles of ProgrammingLanguages, San Francisco, ACM Press, pp. 16–30.
Laurent, O., Quatrini, M., and Tortora de Falco, L., 2005, “Polarizedand focalized linear and classical proofs”,Annals of Pureand Applied Logic, 134 (2–3): 217–264.
Lazic, R. and Schmitz, S., 2015, “Nonelementary complexities forbranching VASS, MELL, and extensions”,ACM Transactions onComputational Logic, 16(3): pp. 20:1–20:30.
Liang, C. and Miller, D., 2009, “Focusing and Polarization in Linear,Intuitionistic, and Classical Logics”,Theoretical ComputerScience, 410(46): 4747–4768.
Lincoln, P., Scedrov, A., and Shankar,N., 1993, “Linearizing intuitionisticimplication”,Annals of Pure and Applied Logic, 60(2):151–177.
Lincoln, P., 1995, “Deciding provability of linear logicformulas”,Proceedings of the Workshop on Advances in LinearLogic, J.-Y. Girard, Y. Lafont, and L. Regnier (eds.), Cambridge:Cambridge University Press, pp. 197–210.
Lincoln, P., Mitchell, J., Scedrov, A., and Shankar, N., 1992, “Decisionproblems for propositional linear logic”,Annals of Pure andApplied Logic, 56: 239–311.
Lincoln, P., and Winkler, T., 1994, “Constant-Only Multiplicative LinearLogic is NP-Complete”,Theoretical Computer Science,135: 155–169.
Martini, S. and Masini, A., 1995, “On the fine structure of theexponential rule”, inAdvances in linear logic, editedby J.-Y. Girard and Y. Lafont and L. Regnier, pp. 197–210, NewYork: Cambridge University Press.
Martin-Löf, P., 1982, “Constructive Mathematics and ComputerProgramming”,Sixth International Congress for Logic,Methodology, and Philosophy of Science, Amsterdam: North-Holland,pp. 153–175.
Melliès, P.-A., Tabareau, N.and Tasson, C., 2018, “An explicit formula for the freeexponential modality of linear logic”,Mathematical Structures in Computer Science, 28(7):1253–1286.
Miller, D., 1996, “Forum: A multiple-conclusion specificationlanguage”,Theoretical Computer Science, 165(1):201–232.
–––, 2003, “Encryption as an abstract data-type: An extendedabstract”, in I. Cervesato (ed.),16th Workshop onFoundations of Computer Security, Asilomar, IEEE ComputingSociety, pp. 3–14, 2003.
–––, 2004, “Overview of linear logic programming”,LinearLogic in Computer Science, T. Ehrhard, J.-Y. Girard, P. Ruet, andP. Scott (eds.) (London Mathematical Society Lecture Notes: Volume316), Cambridge: Cambridge University Press, pp. 119–150.
Murawski, A. S., and Ong, C.-H. L., 2006, “Fast verification of MLL proofnets via IMLL”,ACM Transactions on ComputationalLogic, 7(3): 473–498.
Nigam, V. and Miller, D., 2009, “Algorithmic specifications in linearlogic with subexponentials”, Proceedings of the 11th ACM SIGPLANconference on Principles and practice of declarative programming(PPDP), 2009, pp. 129–140.
Okada, M., 1999, “PhaseSemantic Cut-Elimination and Normalization Proofs of First- andHigher-Order Linear Logic”,TheoreticalComputer Science, 227(1–2): 333–396.
Ono, H., 1998, “Proof-theoreticmethods in nonclassical logic. An Introduction”, inM. Takahashi, M. Okada, and M. Dezani-Ciancaglini (eds.),Theories of Types and Proofs (Mathematical Society of JapanMemoirs: Volume 2), 207–254. doi:10.2969/msjmemoirs/00201C060
Read, S., 1988,Relevant Logic, Oxford: Blackwell.
Retoré, C., 1997, “Pomset logic: a non-commutative extension ofclassical linear logic”,Typed Lambda Calculi andApplications (Lecture notes in Computer Science: Volume 1210),Berlin: Springer Verlag, pp. 300–318.
Retoré, C., 2003, “Handsome proof-nets: perfect matchings and cographs”,Theoretical Computer Science, 294(3): 473–488.
Reutenauer, C., 1989, “Aspects mathématiques des réseaux dePetri”, Etudes et Recherches en Informatique. Masson.
Schellinx, H., 1991, “SomeSyntactical Observations on Linear Logic”,Journal of Logicand Computation, 1(4): 537–559.
Tortora de Falco, L., 2003,“Obsessional experiments for linear logic proof-nets”,Mathematical Structures in Computer Science, 13(6):799–855.
Troelstra, A. S., 1992,“Lectures on Linear Logic”,CSLI Lecture Notes(Number 29), Stanford: CSLI Publications.
Straßburger, L., 2019, “On the Decision Problem for MELL”,Theoretical Computer Science, 768: 91–98.doi:10.1016/j.tcs.2019.02.022
Urquhart, A., 2000, “The Complexity of Linear Logic withWeakening”,Logic Colloquium ’98 (Lecture Notesin Logic 13), Urbana: Association for Symbolic Logic, pp.500–515.
Wadler, P., 1991, “Is there a use for linear logic?”,Proceedings of ACM/SIGPLAN Workshop Partial Evaluation andSemantics-Based Program Manipulation, New Haven: ACM Press, pp.255–273, 1991.
Yetter, D.N., 1990, “Quantales and (noncommutative) linearlogic”,Journal of Symbolic Logic, 55(1):41–64.

Academic Tools

How to cite this entry.
Preview the PDF version of this entry at theFriends of the SEP Society.
Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
Enhanced bibliography for this entryatPhilPapers, with links to its database.

Other Internet Resources

Thelinear logic bibliography (up to 1998).
Vincent Danos and Roberto Di Cosmo.The Linear Logic Primer. Course Notes. (1992).

Acknowledgment

We thank an anonymous reviewer at the SEP for many comments that havehelped us revise this article.

Open access to the SEP is made possible by a world-wide funding initiative.
The Encyclopedia Now Needs Your Support
Please Read How You Can Help Keep the Encyclopedia Free

Browse

About

Support SEP

Mirror Sites

View this site from another server:

USA (Main Site)Philosophy, Stanford University

Info about mirror sites

Library of Congress Catalog Data: ISSN 1095-5054

Movatterモバイル変換