nLab
linear type theory

Contents

Context

Type theory

Monoidal categories

</head> <body> <p><strong><a class='existingWikiWord' href='/nlab/show/monoidal+categories'>monoidal categories</a></strong></p> <h2 id='with_symmetry'>With symmetry</h2> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/braided+monoidal+category'>braided monoidal category</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/balanced+monoidal+category'>balanced monoidal category</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/twist'>twist</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/symmetric+monoidal+category'>symmetric monoidal category</a></p> </li> </ul> <h2 id='with_duals_for_objects'>With duals for objects</h2> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/category+with+duals'>category with duals</a> (list of them)</p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/dualizable+object'>dualizable object</a> (what they have)</p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/rigid+monoidal+category'>rigid monoidal category</a>, a.k.a. <a class='existingWikiWord' href='/nlab/show/autonomous+category'>autonomous category</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/pivotal+category'>pivotal category</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/spherical+category'>spherical category</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/ribbon+category'>ribbon category</a>, a.k.a. <a class='existingWikiWord' href='/nlab/show/tortile+category'>tortile category</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/compact+closed+category'>compact closed category</a></p> </li> </ul> <h2 id='with_duals_for_morphisms'>With duals for morphisms</h2> <ul> <li> <p><span class='newWikiWord'>monoidal dagger-category<a href='/nlab/new/monoidal+dagger-category'>?</a></span></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/symmetric+monoidal+dagger-category'>symmetric monoidal dagger-category</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/dagger+compact+category'>dagger compact category</a></p> </li> </ul> <h2 id='with_traces'>With traces</h2> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/trace'>trace</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/traced+monoidal+category'>traced monoidal category</a></p> </li> </ul> <h2 id='closed_structure'>Closed structure</h2> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/closed+monoidal+category'>closed monoidal category</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/cartesian+closed+category'>cartesian closed category</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/closed+category'>closed category</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/star-autonomous+category'>star-autonomous category</a></p> </li> </ul> <h2 id='special_sorts_of_products'>Special sorts of products</h2> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/cartesian+monoidal+category'>cartesian monoidal category</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/semicartesian+monoidal+category'>semicartesian monoidal category</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/multicategory'>multicategory</a></p> </li> </ul> <h2 id='semisimplicity'>Semisimplicity</h2> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/semisimple+category'>semisimple category</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/fusion+category'>fusion category</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/modular+tensor+category'>modular tensor category</a></p> </li> </ul> <h2 id='morphisms'>Morphisms</h2> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/monoidal+functor'>monoidal functor</a></p> <p>(<a class='existingWikiWord' href='/nlab/show/lax+monoidal+functor'>lax</a>, <a class='existingWikiWord' href='/nlab/show/oplax+monoidal+functor'>oplax</a>, <a class='existingWikiWord' href='/nlab/show/strong+monoidal+functor'>strong</a> <a class='existingWikiWord' href='/nlab/show/bilax+monoidal+functor'>bilax</a>, <a class='existingWikiWord' href='/nlab/show/Frobenius+monoidal+functor'>Frobenius</a>)</p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/braided+monoidal+functor'>braided monoidal functor</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/symmetric+monoidal+functor'>symmetric monoidal functor</a></p> </li> </ul> <h2 id='internal_monoids'>Internal monoids</h2> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/monoid+in+a+monoidal+category'>monoid in a monoidal category</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/commutative+monoid+in+a+symmetric+monoidal+category'>commutative monoid in a symmetric monoidal category</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/module+over+a+monoid'>module over a monoid</a></p> </li> </ul> <h2 id='examples'>Examples</h2> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/tensor+product'>tensor product</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/closed+monoidal+structure+on+presheaves'>closed monoidal structure on presheaves</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/Day+convolution'>Day convolution</a></p> </li> </ul> <h2 id='theorems'>Theorems</h2> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/coherence+theorem+for+monoidal+categories'>coherence theorem for monoidal categories</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/monoidal+Dold-Kan+correspondence'>monoidal Dold-Kan correspondence</a></p> </li> </ul> <h2 id='in_higher_category_theory'>In higher category theory</h2> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/monoidal+2-category'>monoidal 2-category</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/braided+monoidal+2-category'>braided monoidal 2-category</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/monoidal+bicategory'>monoidal bicategory</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/cartesian+bicategory'>cartesian bicategory</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/k-tuply+monoidal+n-category'>k-tuply monoidal n-category</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/little+cubes+operad'>little cubes operad</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/monoidal+%28%E2%88%9E%2C1%29-category'>monoidal (∞,1)-category</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/symmetric+monoidal+%28%E2%88%9E%2C1%29-category'>symmetric monoidal (∞,1)-category</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/compact+double+category'>compact double category</a></p> </li> </ul> <div> <p><a href='/nlab/edit/monoidal+categories+-+contents'>Edit this sidebar</a></p> </div></body></html></div> <h4 id="linear_algebra">Linear algebra</h4> <div class="hide"><html xml:lang='en' xmlns:svg='http://www.w3.org/2000/svg' xmlns='http://www.w3.org/1999/xhtml'> <head><meta content='application/xhtml+xml;charset=utf-8' http-equiv='Content-type' /><title /></head> <body> <p><strong><a class='existingWikiWord' href='/nlab/show/homotopy+theory'>homotopy theory</a>, <a class='existingWikiWord' href='/nlab/show/%28%E2%88%9E%2C1%29-category+theory'>(∞,1)-category theory</a>, <a class='existingWikiWord' href='/nlab/show/homotopy+type+theory'>homotopy type theory</a></strong></p> <p>flavors: <a class='existingWikiWord' href='/nlab/show/stable+homotopy+theory'>stable</a>, <a class='existingWikiWord' href='/nlab/show/equivariant+homotopy+theory'>equivariant</a>, <a class='existingWikiWord' href='/nlab/show/rational+homotopy+theory'>rational</a>, <a class='existingWikiWord' href='/nlab/show/p-adic+homotopy+theory'>p-adic</a>, <a class='existingWikiWord' href='/nlab/show/proper+homotopy+theory'>proper</a>, <a class='existingWikiWord' href='/nlab/show/geometric+homotopy+theory'>geometric</a>, <a class='existingWikiWord' href='/nlab/show/cohesive+homotopy+theory'>cohesive</a>, <a class='existingWikiWord' href='/nlab/show/directed+homotopy+theory'>directed</a>…</p> <p>models: <a class='existingWikiWord' href='/nlab/show/topological+homotopy+theory'>topological</a>, <a class='existingWikiWord' href='/nlab/show/simplicial+homotopy+theory'>simplicial</a>, <a class='existingWikiWord' href='/nlab/show/localic+homotopy+theory'>localic</a>, …</p> <p>see also <strong><a class='existingWikiWord' href='/nlab/show/algebraic+topology'>algebraic topology</a></strong></p> <p><strong>Introductions</strong></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/Introduction+to+Topology+--+2'>Introduction to Basic Homotopy Theory</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/Introduction+to+Homotopy+Theory'>Introduction to Abstract Homotopy Theory</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/geometry+of+physics+--+homotopy+types'>geometry of physics – homotopy types</a></p> </li> </ul> <p><strong>Definitions</strong></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/homotopy'>homotopy</a>, <a class='existingWikiWord' href='/nlab/show/higher+homotopy'>higher homotopy</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/homotopy+type'>homotopy type</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/Pi-algebra'>Pi-algebra</a>, <a class='existingWikiWord' href='/nlab/show/spherical+object+and+Pi%28A%29-algebra'>spherical object and Pi(A)-algebra</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/homotopy+coherent+category+theory'>homotopy coherent category theory</a></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/homotopical+category'>homotopical category</a></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/model+category'>model category</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/category+of+fibrant+objects'>category of fibrant objects</a>, <a class='existingWikiWord' href='/nlab/show/cofibration+category'>cofibration category</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/Waldhausen+category'>Waldhausen category</a></p> </li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/homotopy+category'>homotopy category</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/Ho%28Top%29'>Ho(Top)</a></li> </ul> </li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/%28%E2%88%9E%2C1%29-category'>(∞,1)-category</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/homotopy+category+of+an+%28%E2%88%9E%2C1%29-category'>homotopy category of an (∞,1)-category</a></li> </ul> </li> </ul> <p><strong>Paths and cylinders</strong></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/left+homotopy'>left homotopy</a></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/cylinder+object'>cylinder object</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/mapping+cone'>mapping cone</a></p> </li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/right+homotopy'>right homotopy</a></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/path+object'>path object</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/mapping+cocone'>mapping cocone</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/generalized+universal+bundle'>universal bundle</a></p> </li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/interval+object'>interval object</a></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/homotopy+localization'>homotopy localization</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/infinitesimal+interval+object'>infinitesimal interval object</a></p> </li> </ul> </li> </ul> <p><strong>Homotopy groups</strong></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/homotopy+group'>homotopy group</a></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/fundamental+group'>fundamental group</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/fundamental+group+of+a+topos'>fundamental group of a topos</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/Brown-Grossman+homotopy+group'>Brown-Grossman homotopy group</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/categorical+homotopy+groups+in+an+%28%E2%88%9E%2C1%29-topos'>categorical homotopy groups in an (∞,1)-topos</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/geometric+homotopy+groups+in+an+%28%E2%88%9E%2C1%29-topos'>geometric homotopy groups in an (∞,1)-topos</a></p> </li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/fundamental+%E2%88%9E-groupoid'>fundamental ∞-groupoid</a></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/fundamental+groupoid'>fundamental groupoid</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/path+groupoid'>path groupoid</a></li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/fundamental+%E2%88%9E-groupoid+in+a+locally+%E2%88%9E-connected+%28%E2%88%9E%2C1%29-topos'>fundamental ∞-groupoid in a locally ∞-connected (∞,1)-topos</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/fundamental+%E2%88%9E-groupoid+of+a+locally+%E2%88%9E-connected+%28%E2%88%9E%2C1%29-topos'>fundamental ∞-groupoid of a locally ∞-connected (∞,1)-topos</a></p> </li> </ul> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/fundamental+%28%E2%88%9E%2C1%29-category'>fundamental (∞,1)-category</a></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/fundamental+category'>fundamental category</a></li> </ul> </li> </ul> <p><strong>Basic facts</strong></p> <ul> <li><a class='existingWikiWord' href='/nlab/show/fundamental+group+of+the+circle+is+the+integers'>fundamental group of the circle is the integers</a></li> </ul> <p><strong>Theorems</strong></p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/fundamental+theorem+of+covering+spaces'>fundamental theorem of covering spaces</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/Freudenthal+suspension+theorem'>Freudenthal suspension theorem</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/Blakers-Massey+theorem'>Blakers-Massey theorem</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/higher+homotopy+van+Kampen+theorem'>higher homotopy van Kampen theorem</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/nerve+theorem'>nerve theorem</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/Whitehead%27s+theorem'>Whitehead's theorem</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/Hurewicz+theorem'>Hurewicz theorem</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/Galois+theory'>Galois theory</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/homotopy+hypothesis'>homotopy hypothesis</a>-theorem</p> </li> </ul> </body></html></div> </div> </div> <h1 id="contents">Contents</h1> <div class="maruku_toc"><ul><li><a href="#idea">Idea</a></li><li><a href="#properties">Properties</a><ul><li><a href="#categorical_semantics">Categorical semantics</a></li><li><a href="#the_canonical_comodality">The canonical co-modality</a></li></ul></li><li><a href="#HistoryCategoricalSemantics">History of linear categorical semantics</a></li><li><a href="#related_concepts">Related concepts</a></li><li><a href="#references">References</a><ul><li><a href="#general">General</a></li><li><a href="#lambeks_syntactic_calculus">Lambek’s syntactic calculus</a></li><li><a href="#categorical_semantics_2">Categorical semantics</a></li></ul></li></ul></div> <h2 id="idea">Idea</h2> <p><em>Linear type theory</em> is the <a class='existingWikiWord' href='/nlab/show/linear+logic'>linear logic</a>-version of <a class='existingWikiWord' href='/nlab/show/type+theory'>type theory</a>. In the definition of (<a href="#Seely89">Seely 89, prop. 1.5</a>), following (<a href="#Girard87">Girard 87</a>), this is the <a class='existingWikiWord' href='/nlab/show/internal+language'>internal language</a> of/has <a class='existingWikiWord' href='/nlab/show/categorical+semantics'>categorical semantics</a> in <a class='existingWikiWord' href='/nlab/show/star-autonomous+categories'>star-autonomous categories</a>.</p> <p>More generally, the term “linear” (as in <em>linear type theory</em>) has over time come to connote <a class='existingWikiWord' href='/nlab/show/internal+languages'>internal</a> <a class='existingWikiWord' href='/nlab/show/type+theories'>type theories</a>, and related logical frameworks (<a class='existingWikiWord' href='/nlab/show/sequent+calculus'>sequent calculi</a>, <a class='existingWikiWord' href='/nlab/show/natural+deduction'>natural deduction</a>) that correspond to (usually symmetric) monoidal categories, where particularly the monoidal product is not assumed to be the cartesian product (reviews include <a href="#BlutePanangadenSeely94">Blute-Panangaden-Seely 94</a>). Indeed, this general notion still faithfully follows the original motivation for the term “linear” as introduced in (<a href="#Girard87">Girard 87</a>), since the non-cartesianness of the <a class='existingWikiWord' href='/nlab/show/tensor+product'>tensor product</a> means the absence of a <a class='existingWikiWord' href='/nlab/show/diagonal'>diagonal</a> map and hence the impossibility of <a class='existingWikiWord' href='/nlab/show/functions'>functions</a> to depend on more than a single (linear) copy of their <a class='existingWikiWord' href='/nlab/show/variables'>variables</a>.</p> <p>In the corresponding logical frameworks, the non-cartesianness means one drops the contraction and weakening rules of inference associated with cartesian structure, but retains the exchange rule corresponding to the symmetry constraint. This general type of “linear logic” takes on many flavors: in addition to the Girard-style language that is naturally interpreted in <a class='existingWikiWord' href='/nlab/show/star-autonomous+categories'>star-autonomous categories</a>, one has languages for <a class='existingWikiWord' href='/nlab/show/closed+monoidal+category'>monoidal biclosed categories</a>, <a class='existingWikiWord' href='/nlab/show/closed+monoidal+category'>symmetric monoidal closed categories</a>, <a class='existingWikiWord' href='/nlab/show/compact+closed+categories'>compact closed categories</a>, and others, collectively representing the “multiplicative” core of linear logic as understood in this general sense.</p> <p>In addition to this “multiplicative” core, one also often studies modalities (comonads) which relate these symmetric monoidal products to cartesian products and coproducts (so-called “additive” operations in linear logic).</p> <p>Extending these considerations, the <a class='existingWikiWord' href='/nlab/show/dependent+type+theory'>dependent type theory</a>-version of linear type theory should be <em><a class='existingWikiWord' href='/nlab/show/dependent+linear+type+theory'>dependent linear type theory</a></em>.</p> <p>Linear (dependent) type theory can be argued to be the proper <a class='existingWikiWord' href='/nlab/show/type+theory'>type theory</a> for <a class='existingWikiWord' href='/nlab/show/quantum+logic'>quantum logic</a>. In this context the linearity of the type theory, hence the absence of <a class='existingWikiWord' href='/nlab/show/diagonal+maps'>diagonal maps</a> in its <a class='existingWikiWord' href='/nlab/show/categorical+semantics'>categorical semantics</a>, corresponds to the <a class='existingWikiWord' href='/nlab/show/no-cloning+theorem'>no-cloning theorem</a> in <a class='existingWikiWord' href='/nlab/show/quantum+physics'>quantum physics</a>.</p> <h2 id="properties">Properties</h2> <h3 id="categorical_semantics">Categorical semantics</h3> <p>(…)</p> <p>In <a class='existingWikiWord' href='/nlab/show/star-autonomous+categories'>star-autonomous categories</a>.</p> <table><thead><tr><th>Conjunctive operator</th><th><math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>←</mo></mrow><annotation encoding='application/x-tex'>\leftarrow</annotation></semantics></math><a class='existingWikiWord' href='/nlab/show/de+Morgan+duality'>de Morgan duality</a> <math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>→</mo></mrow><annotation encoding='application/x-tex'>\rightarrow</annotation></semantics></math></th><th>Disjunctive operator</th></tr></thead><tbody><tr><td style="text-align: left;"><math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>⊤</mo></mrow><annotation encoding='application/x-tex'>\top</annotation></semantics></math></td><td style="text-align: left;"></td><td style="text-align: left;"><math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>0</mn></mrow><annotation encoding='application/x-tex'>0</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mn>1</mn></mrow><annotation encoding='application/x-tex'>1</annotation></semantics></math></td><td style="text-align: left;"></td><td style="text-align: left;"><math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>⊥</mo></mrow><annotation encoding='application/x-tex'>\bot</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>&</mi></mrow><annotation encoding='application/x-tex'>\&</annotation></semantics></math></td><td style="text-align: left;"></td><td style="text-align: left;"><math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>⊕</mo></mrow><annotation encoding='application/x-tex'>\oplus</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>⊗</mo></mrow><annotation encoding='application/x-tex'>\otimes</annotation></semantics></math></td><td style="text-align: left;"></td><td style="text-align: left;"><math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>⅋</mo></mrow><annotation encoding='application/x-tex'>\parr</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msup><mo /><mo>⊥</mo></msup></mrow><annotation encoding='application/x-tex'>^\bot</annotation></semantics></math></td><td style="text-align: left;"></td><td style="text-align: left;"><math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><msup><mo /><mo>⊥</mo></msup></mrow><annotation encoding='application/x-tex'>^\bot</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo lspace='thinmathspace' rspace='thinmathspace'>⋀</mo></mrow><annotation encoding='application/x-tex'>\bigwedge</annotation></semantics></math></td><td style="text-align: left;"></td><td style="text-align: left;"><math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo lspace='thinmathspace' rspace='thinmathspace'>⋁</mo></mrow><annotation encoding='application/x-tex'>\bigvee</annotation></semantics></math></td></tr> <tr><td style="text-align: left;"><math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>!</mo></mrow><annotation encoding='application/x-tex'>!</annotation></semantics></math></td><td style="text-align: left;"></td><td style="text-align: left;"><math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>?</mo></mrow><annotation encoding='application/x-tex'>?</annotation></semantics></math></td></tr> </tbody></table> <p>(…)</p> <h3 id="the_canonical_comodality">The canonical co-modality</h3> <p>The original axiomatics for <a class='existingWikiWord' href='/nlab/show/linear+type+theory'>linear type theory</a> in (<a href="#Girard87">Girard 87</a>) contain in addition to the structures corresponding to a (<a class='existingWikiWord' href='/nlab/show/star-autonomous+category'>star-autonomous</a>) <a class='existingWikiWord' href='/nlab/show/symmetric+monoidal+category'>symmetric</a> <a class='existingWikiWord' href='/nlab/show/closed+monoidal+category'>closed monoidal category</a> a certain (co-)<a class='existingWikiWord' href='/nlab/show/modality'>modality</a> traditionally denoted “<math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>!</mo></mrow><annotation encoding='application/x-tex'>!</annotation></semantics></math>”, the [[!-modality]]. In (<a href="#Benton95">Benton 95</a>, <a href="#Bierman95">Bierman 95</a>) it is noticed (reviewed in (<a href="#Barber97">Barber 97, p. 21 (26)</a>)) that a natural <a class='existingWikiWord' href='/nlab/show/categorical+semantics'>categorical semantics</a> for this modality identifies it with the <a class='existingWikiWord' href='/nlab/show/comonad'>comonad</a> that is induced from a <a class='existingWikiWord' href='/nlab/show/strong+monoidal+adjunction'>strong monoidal adjunction</a></p> <div class="maruku-equation"><math class='maruku-mathml' display='block' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo stretchy='false'>(</mo><mi>Σ</mi><mo>⊣</mo><mi>R</mi><mo stretchy='false'>)</mo><mspace width='thickmathspace' /><mo lspace='verythinmathspace'>:</mo><mspace width='thickmathspace' /><mi>𝒞</mi><mover><munder><mo>⟶</mo><mi>R</mi></munder><mover><mo>←</mo><mi>Σ</mi></mover></mover><mi>S</mi></mrow><annotation encoding='application/x-tex'> (\Sigma \dashv R) \;\colon\; \mathcal{C} \stackrel{\overset{\Sigma}{\leftarrow}}{\underset{R}{\longrightarrow}} S </annotation></semantics></math></div> <p>between the <a class='existingWikiWord' href='/nlab/show/closed+monoidal+category'>closed</a> <a class='existingWikiWord' href='/nlab/show/symmetric+monoidal+category'>symmetric monoidal category</a> <math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>𝒞</mi></mrow><annotation encoding='application/x-tex'>\mathcal{C}</annotation></semantics></math> wich interprets the given <a class='existingWikiWord' href='/nlab/show/linear+type+theory'>linear type theory</a> and a <a class='existingWikiWord' href='/nlab/show/cartesian+monoidal+category'>cartesian monoidal category</a> <math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math>.</p> <p>If there is only the <a class='existingWikiWord' href='/nlab/show/strong+monoidal+functor'>strong monoidal functor</a> <math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>Σ</mi><mspace width='thickmathspace' /><mo lspace='verythinmathspace'>:</mo><mspace width='thickmathspace' /><mi>S</mi><mo>⟶</mo><mi>𝒞</mi></mrow><annotation encoding='application/x-tex'>\Sigma \;\colon\; S \longrightarrow \mathcal{C}</annotation></semantics></math> without possibly a <a class='existingWikiWord' href='/nlab/show/right+adjoint'>right adjoint</a>, then (<a href="#Barber97">Barber 97, p. 21 (27)</a>) speaks of the <em>structural <a class='existingWikiWord' href='/nlab/show/fragment'>fragment</a></em> of <a class='existingWikiWord' href='/nlab/show/linear+type+theory'>linear type theory</a>.</p> <p>In (<a href="#PontoShulman12">Ponto-Shulman 12</a>) it is observed that this in turn is canonically induced if <math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>𝒞</mi><mo>≃</mo><msub><mi>𝒞</mi> <mo>*</mo></msub></mrow><annotation encoding='application/x-tex'>\mathcal{C} \simeq \mathcal{C}_\ast</annotation></semantics></math> is the linear type theory over the trivial context of a <a class='existingWikiWord' href='/nlab/show/dependent+linear+type+theory'>dependent linear type theory</a>/<a class='existingWikiWord' href='/nlab/show/indexed+closed+monoidal+category'>indexed closed monoidal category</a> with category of contexts being <math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mi>S</mi></mrow><annotation encoding='application/x-tex'>S</annotation></semantics></math>. See at <em><a href="http://ncatlab.org/nlab/show/dependent+linear+type+theory#TheCanonicalComodality">dependent linear type theory – Properties – Canonical co-modality</a></em> for more on this.</p> <h2 id="HistoryCategoricalSemantics">History of linear categorical semantics</h2> <p>There is a long history of logical frameworks of “linear type” and their categorical semantics in various <a class='existingWikiWord' href='/nlab/show/doctrines'>doctrines</a> of monoidal and closed monoidal categories, even though much of the early history predates Girard’s introduction of linear logic (and which therefore do not bear the term “linear”). We give a thumbnail sketch of some of this below.</p> <p>The founding father could be said to be <a class='existingWikiWord' href='/nlab/show/Joachim+Lambek'>Joachim Lambek</a>, who was the first to apply deductive systems and particularly the method of Gentzen cut-elimination to what we would now recognize as <a class='existingWikiWord' href='/nlab/show/categorification'>categorification</a>s of various <a class='existingWikiWord' href='/nlab/show/fragments'>fragments</a> of propositional logic. It is noteworthy that one of the various first applications of this categorified cut-elimination was to the (<em>linear</em>) doctrine of <a class='existingWikiWord' href='/nlab/show/monoidal+biclosed+categories'>monoidal biclosed categories</a>, in which Lambek was interested in connection with his linguistic research (<a href="#Lambek58">Lambek 58</a>); see (<a href="#Lambek68">Lambek 68</a>, <a href="#Lambek69">Lambek 69</a>). A principal goal in these papers was to study (and partially solve) the coherence problem for such structures.</p> <div class="num_remark"> <h6 id="remark">Remark</h6> <p>Kelly and Mac Lane then adapted the essential cut-elimination techniques of Lambek to study the (difficult) coherence problem for closed symmetric monoidal categories, in their landmark study <a href="#KM71">KM</a>. Their work cleverly avoided the explicit introduction of logical equipment, presumably in the service of greater self-containment or greater categorical readership, although the debt to Lambek’s pioneering work is clear enough (and <em>is</em> made explicit).</p> </div> <p>By the late 1970‘s, the connections between <a class='existingWikiWord' href='/nlab/show/proof+theory'>proof theory</a>, coherence theory, and the categorical semantics of deductive systems had been well elaborated, and again it is noteworthy that there was especial focus on categorical doctrines of general linear type. A largish batch of various <a class='existingWikiWord' href='/nlab/show/fragments'>fragments</a> of classical logic, particularly in sequent calculus form, together with their categorical semantics, was collected in a book-length study (<a href="#Szabo78">Szabo 78</a>) by Manfred Szabo, who had been Lambek’s student. (While the categorical semantics of various deductive systems were carefully spelled out in Szabo’s book, this work was unfortunately tainted by overly ambitious claims by Szabo regarding his purported solutions to the relevant coherence problems, in terms of normalization algorithms which turned out not to be Church-Rosser; see <a href="#Jay90a">Jay 90a</a>.)</p> <p>Nor were the logical frameworks restricted to those of sequent calculus type. In particular, the Soviet logician Minc and his students had also developed a type theory whose semantics is naturally valued in closed monoidal categories; see <a href="#Minc77">Minc 77</a>. This too was in view of coherence problems.</p> <p>Interest in these problems was of course reawakened and reinvigorated in the light of Girard’s extraordinarily insightful 1987 paper <a href="#Girard87">Linear Logic</a>. The connection with closed symmetric monoidal categories and <math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>*</mo></mrow><annotation encoding='application/x-tex'>\ast</annotation></semantics></math>-autonomous categories was picked up in very short order by the categorical community; an early account of this connection was given by <a href="#Seely89">Seely 89</a>. It was not long before Girard’s very fruitful exposition of linear proof theory and <a class='existingWikiWord' href='/nlab/show/cut-elimination'>cut-elimination</a> in terms of <a class='existingWikiWord' href='/nlab/show/proof+net'>proof nets</a>, specifically for the <a class='existingWikiWord' href='/nlab/show/multiplicative+conjunction'>multiplicative</a> <a class='existingWikiWord' href='/nlab/show/fragment'>fragment</a> MLL which is the basic technical core of Girard’s work, was seen as closely related to “extranaturality” graphs (aka KM-graphs) used by Kelly-Mac Lane in their work on the coherence theory for closed symmetric monoidal categories – as well as by other “Australian category theorists” who had developed Kelly’s theory of clubs (which again tended to be most successful for doctrines of linear type).</p> <p>These aspects are covered in (<a href="#Blute91">Blute 91</a>), who treated a number of coherence problems and particularly the method of Lambek/Kelly-Mac Lane as efficiently streamlined through the method of proof nets with connection given to KM-graphs and clubs. Note that all of those applications were towards various <a class='existingWikiWord' href='/nlab/show/fragments'>fragments</a> of MLL or doctrines of linear type.</p> <p>From approximately the same time period we also have some work of Barry Jay, who had developed a calculus of terms and their normalization to study coherence for closed monoidal categories. See for instance (<a href="#Jay89">Jay 89</a>, <a href="#Jay90b">Jay 90b</a>). (This does not seem to owe allegiance to Girard’s methods particularly, but it does indicate some contemporaneous thinking on linear types, terms, and their categorical semantics.)</p> <div class="num_remark"> <h6 id="remark_2">Remark</h6> <p>It should be noted that the “classical” techniques developed by Lambek, Kelly-Mac Lane, and Blute merely yield <em>partial</em> coherence results, in effect evading the notorious “problem of the unit” which had made the full coherence problem for closed monoidal categories seem fearsomely difficult. However, Trimble in his (unpublished) 1994 thesis showed how to re-interpret Girard’s proof nets so that they naturally took the unit into account, and was then able to give a <em>full</em> coherence result for MILL by arranging cut-free nets into a strongly normalizing and confluent rewrite system. Note that while full coherence results for this case had also been proposed by Voreadou and Dole (students of Mac Lane), by Minc and Jay, and also incorrectly by Szabo, none of these earlier approaches were in a position to take advantage of the proof net formalism. For another account of this sort of formalism, specifically for the case of <math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>*</mo></mrow><annotation encoding='application/x-tex'>\ast</annotation></semantics></math>-autonomous categories, <a class='existingWikiWord' href='/nlab/show/weakly+distributive+category'>weakly distributive categories</a>, and full coherence thereof, see <a href="#BluteCockettSeelyTrimble96">Blute-Cockett-Seely-Trimble96</a>.</p> </div> <p>Meanwhile, the type theory and its categorical semantics for <em>full</em> linear logic, going beyond MLL and taking into account the modalities and the “additive” operations of LL, was also advanced during this time period. A comprehensive description is given in <a href="#BentonBiermanPaivaHyland92">Benton-Bierman-de Paiva-Hyland 92</a>, with an important antecedent in de Paiva’s work on the Dialectica interpretation <a href="#dePaiva89">de Paiva 89</a>. See also <a href="#HylandPaiva93">Hyland-de Paiva 93</a>, <a href="#Bierman95">Bierman 95</a>, <a href="#Barber97">Barber 97</a></p> <p>See also <a href="#Schalk04">Schalk 04</a>, <a href="#Mellies09">Melliès 09</a>. Schalk and Melliès have also worked on game-theoretic semantics of theories of linear type – which itself has a long and intricate history.</p> <p>Finally, in addition to these usual “denotational” categorical semantica, linear logic also has an “operational” categorical semantics, called the Geometry of Interaction, in traced monoidal categories.</p> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/propositions+as+projections'>propositions as projections</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/modal+type+theory'>modal type theory</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/geometric+homotopy+type+theory'>geometric homotopy type theory</a></p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/stable+homotopy+type'>stable homotopy type</a></p> </li> </ul> <h2 id="references">References</h2> <h3 id="general">General</h3> <p>The original article on <a class='existingWikiWord' href='/nlab/show/linear+logic'>linear logic</a> is</p> <ul> <li id="Girard87"><a class='existingWikiWord' href='/nlab/show/Jean-Yves+Girard'>Jean-Yves Girard</a>, <em>Linear logic</em>, Theoretical Computer Science 50:1, 1987. (<a href="http://iml.univ-mrs.fr/~girard/linear.pdf">pdf</a>)</li> </ul> <p>A review of linear logic is in</p> <ul> <li id="Girard11"><a class='existingWikiWord' href='/nlab/show/Jean-Yves+Girard'>Jean-Yves Girard</a>, part III of <em><a class='existingWikiWord' href='/nlab/show/Lectures+on+Logic'>Lectures on Logic</a></em>, European Mathematical Society 2011</li> </ul> <p>Linear type theory as such is made explicit for instance in</p> <ul> <li> <p>Masahito Hasegawa. <em>Logical predicates for intuitionistic linear type theories</em>, Typed Lambda Calculi and Applications: 4th International Conference, TLCA ‘99, ed. J.-Y. Girard, Lecture Notes in Computer Science 1581, Springer, Berlin, 1999 (<a href="http://www.kurims.kyoto-u.ac.jp/~hassei/papers/tlca99.pdf">pdf</a>)</p> </li> <li> <p><a href="http://www.cs.cmu.edu/~fp/courses/15816-f01/handouts/lintt.pdf">pdf</a></p> </li> </ul> <h3 id="lambeks_syntactic_calculus">Lambek’s syntactic calculus</h3> <p>Several decades before Girard’s article on linear logic, Lambek introduced a sequent calculus without weakening, contraction, or exchange, and described its applications to modeling aspects of natural language (generalizing previous work by Ajdukiewicz and Bar-Hillel on <a class='existingWikiWord' href='/nlab/show/categorial+grammar'>categorial grammar</a>):</p> <ul> <li id="Lambek58"><a class='existingWikiWord' href='/nlab/show/Joachim+Lambek'>Joachim Lambek</a>. <em>The mathematics of sentence structure</em> . American mathematical monthly, 154-170, 1958. <a href="http://www.jstor.org/stable/2310058">link</a></li> </ul> <p>Lambek called his system the “syntactic calculus”, while nowadays it is often called <em>Lambek calculus</em> in linguistics.</p> <p>In “Towards a geometry of interaction” (1989), Girard references Lambek’s 1958 article, and writes that “this work must be acknowledged as a true ancestor to linear logic; its connection to linguistics can be seen as the first serious evidence against the exclusive focus on mathematics” (p.81). On the other hand, Lambek later wrote that his original motivations were actually in <a class='existingWikiWord' href='/nlab/show/homological+algebra'>homological algebra</a>:</p> <blockquote> <p>I would now call this system “bilinear logic”, meaning “non-commutative linear logic” or “logic without Gentzen’s three structural rules”. My original name had been “syntactic calculus”, because of its intended application to linguistics; but actually it had been developed in collaboration with George Findlay [1955] in an attempt to understand some basic homological algebra. Alas, our paper was rejected on the grounds that most of our results were to appear in a book by Cartan and Eilenberg [1956], the publication of which had been delayed because of a paper shortage. (Lambek, “Bilinear logic in algebra and linguistics”, <em>Advances in Linear Logic</em>, CUP, 1995)</p> </blockquote> <h3 id="categorical_semantics_2">Categorical semantics</h3> <p>The following articles are about “logics of linear type” and their categorical semantics, although they predate the use of the word “linear” in Girard’s sense. Most have a view motivated in part by categorical coherence problems.</p> <ul> <li id="Lambek68"> <p><a class='existingWikiWord' href='/nlab/show/Joachim+Lambek'>Joachim Lambek</a>, <em>Deductive systems and categories</em>, Mathematical Systems Theory 2 (1968), 287-318.</p> </li> <li id="Lambek69"> <p><a class='existingWikiWord' href='/nlab/show/Joachim+Lambek'>Joachim Lambek</a>, <em>Deductive systems and categories II</em>, Lecture Notes in Math. 86, Springer-Verlag (1969), 76-122.</p> </li> <li id="Minc77"> <p>G.E. Minc, <em>Closed categories and the theory of proofs</em>, translated from an article in Russian in Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Mat. Instituta im. V.A. Steklova AN SSSR 68 (1977), 83-114. Republished in Grigorii E. Mints, <em>Selected Papers in Proof Theory</em>, Bibliopolis (1992).</p> </li> <li id="Szabo78"> <p>M.E. Szabo, <em>Algebra of Proofs</em>, Studies in Logic and the Foundations of Mathematics, vol. 88 (1978), North-Holland.</p> </li> <li id="Jay89"> <p>C.B. Jay, <em>Languages for monoidal categories</em>, JPAA 59 (1989), 61-85.</p> </li> <li id="Jay90a"> <p>C.B. Jay, <em>Coherence in category theory and the Church-Rosser property</em>. Unpublished preprint (1990), cited in the following reference.</p> </li> <li id="Jay90b"> <p>C.B. Jay, <em>The structure of free closed categories</em>, JPAA 66 (1990), 271-285.</p> </li> </ul> <p>The <a class='existingWikiWord' href='/nlab/show/categorical+semantics'>categorical semantics</a> of linear type theory in <a class='existingWikiWord' href='/nlab/show/star-autonomous+categories'>star-autonomous categories</a> was first described in</p> <ul> <li id="Seely89"><a class='existingWikiWord' href='/nlab/show/R.+A.+G.+Seely'>R. A. G. Seely</a>, <em>Linear logic, <math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>*</mo></mrow><annotation encoding='application/x-tex'>\ast</annotation></semantics></math>-autonomous categories and cofree coalgebras</em>, <em>Contemporary Mathematics</em> 92, 1989. (<a class='existingWikiWord' href='/nlab/files/SeelyLinearLogic.pdf' title='pdf'>pdf</a>, <a href="http://www.math.mcgill.ca/rags/nets/llsac.ps.gz">ps.gz</a>)</li> </ul> <p>with the first non-syntactic, mathematical categorical model in the same volume:</p> <ul> <li id="dePaiva89"><a class='existingWikiWord' href='/nlab/show/Valeria+de+Paiva'>Valeria de Paiva</a>, <em>The Dialectica Categories</em>, <em>Contemporary Mathematics</em> 92, 1989. (<a href="http://www.cs.bham.ac.uk/~vdp/publications/dial87.pdf">web</a>)</li> </ul> <p>As mentioned above, generalization of this semantics, restricted to the “multiplicative fragment” but covering doctrines of more general symmetric monoidal closed type (with specific reference to Girard’s work) is given in</p> <ul> <li id="Blute91"><a class='existingWikiWord' href='/nlab/show/Richard+Blute'>Richard Blute</a>, <em>Linear logic, coherence, and dinaturality</em>, Dissertation, University of Pennsylvania 1991, published in Theoretical Computer Science archive Volume 115 Issue 1, (July 5, 1993) 3-41.</li> </ul> <p>Blute’s thesis derives coherence theorems for various doctrines of “linear type”, including a coherence theorem for symmetric monoidal <a class='existingWikiWord' href='/nlab/show/closed+categories'>closed categories</a> due to Kelly and Mac Lane:</p> <ul> <li id="KM71"><a class='existingWikiWord' href='/nlab/show/Max+Kelly'>Max Kelly</a>, <a class='existingWikiWord' href='/nlab/show/Saunders+MacLane'>Saunders MacLane</a>, <em>Coherence in closed categories</em>, JPAA 1 (1971), 97-140 (<a href="http://www.sciencedirect.com/science/article/pii/0022404971900132">web</a>)</li> </ul> <p>An decent review of some of this is in</p> <ul> <li id="BlutePanangadenSeely94"><a class='existingWikiWord' href='/nlab/show/Richard+Blute'>Richard Blute</a>, <a class='existingWikiWord' href='/nlab/show/Prakash+Panangaden'>Prakash Panangaden</a>, <a class='existingWikiWord' href='/nlab/show/R.+A.+G.+Seely'>R. A. G. Seely</a>, <em>Fock Space: A Model of Linear Exponential Types</em> (1994) (<a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.6825">web</a>)</li> </ul> <p>Extensions of the coherence-theoretic applications of proof nets in Blute’s thesis, to give full solutions to coherence problems, were given in</p> <ul> <li id="Trimble94"> <p><a class='existingWikiWord' href='/nlab/show/Todd+Trimble'>Todd Trimble</a>, <em>Linear Logic, Bimodules, and Full Coherence for Autonomous Categories, Rutgers 1994</em></p> </li> <li id="BluteCockettSeelyTrimble96"> <p><a class='existingWikiWord' href='/nlab/show/Richard+Blute'>Richard Blute</a>, Cockett, <a class='existingWikiWord' href='/nlab/show/R.+A.+G.+Seely'>R. A. G. Seely</a>, <a class='existingWikiWord' href='/nlab/show/Todd+Trimble'>Todd Trimble</a>, <em>Natural deduction and coherence for weakly distributive categories</em>, JPAA 113 (1996), 229-296. (<a href="http://www.sciencedirect.com/science/article/pii/002240499500159X">web</a>)</p> </li> </ul> <p>Type theory for full linear logic, together with its categorical interpretation, was developed in</p> <ul> <li id="BentonBiermanPaivaHyland92"> <p><a class='existingWikiWord' href='/nlab/show/Nick+Benton'>Nick Benton</a>, Gavin Bierman, <a class='existingWikiWord' href='/nlab/show/Valeria+de+Paiva'>Valeria de Paiva</a>, <a class='existingWikiWord' href='/nlab/show/Martin+Hyland'>Martin Hyland</a>, <em>Term assignments for intuitionistic linear logic</em>. Technical report 262, Cambridge 1992 (<a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.8666">citeseer</a>)</p> </li> <li id="HylandPaiva93"> <p><a class='existingWikiWord' href='/nlab/show/Martin+Hyland'>Martin Hyland</a>, <a class='existingWikiWord' href='/nlab/show/Valeria+de+Paiva'>Valeria de Paiva</a>, <em>Full Intuitionistic Linear Logic</em> (extended abstract). Annals of Pure and Applied Logic, 64(3), pp.273-291, 1993. (<a href="http://www.cs.bham.ac.uk/~vdp/publications/fill.pdf">pdf</a>)</p> </li> <li id="Barber97"> <p>Andrew Graham Barber, <em>Linear Type Theories, Semantics and Action Calculi</em>, PhD Thesis, Edinburgh 1997 (<a href="http://www.lfcs.inf.ed.ac.uk/reports/97/ECS-LFCS-97-371/‎">web</a>, <a href="http://www.lfcs.inf.ed.ac.uk/reports/97/ECS-LFCS-97-371/ECS-LFCS-97-371.pdf">pdf</a>)</p> </li> </ul> <p>Further review and discussion is in</p> <ul> <li id="Bierman95">Gavin M. Bierman, <em>What is a categorical model of intuitionistic linear logic? (<a href="http://research.microsoft.com/en-us/um/people/gmb/papers/tlca95.pdf">web</a>)</em></li> </ul> <p>The more general case of general <a class='existingWikiWord' href='/nlab/show/symmetric+monoidal+categories'>symmetric monoidal categories</a> is reviewed and further discussed in</p> <ul> <li id="Schalk04"> <p>Andrea Schalk, <em>What is a categorical model for linear logic?</em> (<a href="http://www.cs.man.ac.uk/∼schalk/notes/llmodel.pdf">pdf</a>)</p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/Richard+Blute'>Richard Blute</a>, Philip Scott, <em>Category theory for linear logicians</em>, 2004 (<a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.6250">citeseer</a>)</p> </li> <li id="Mellies09"> <p><a class='existingWikiWord' href='/nlab/show/Paul-Andr%C3%A9+Melli%C3%A8s'>Paul-André Melliès</a> , <em>Categorial Semantics of Linear Logic</em>, in <em>Interactive models of computation and program behaviour</em>, Panoramas et synthèses 27, 2009 (<a href="http://www.pps.univ-paris-diderot.fr/~mellies/papers/panorama.pdf">pdf</a>)</p> </li> </ul> <p>The interpretation of Girard’s <math class='maruku-mathml' display='inline' xmlns='http://www.w3.org/1998/Math/MathML'><semantics><mrow><mo>!</mo></mrow><annotation encoding='application/x-tex'>!</annotation></semantics></math>-modality as the <a class='existingWikiWord' href='/nlab/show/comonad'>comonad</a> induced from a <a class='existingWikiWord' href='/nlab/show/monoidal+adjunction'>monoidal adjunction</a> between the closed <a class='existingWikiWord' href='/nlab/show/symmetric+monoidal+category'>symmetric monoidal category</a> and a <a class='existingWikiWord' href='/nlab/show/cartesian+closed+category'>cartesian closed category</a> is due to</p> <ul> <li id="Bierman95"> <p>G. Bierman, <em>On Intuitionistic Linear Logic</em> PhD thesis, Computing Laboratory, University of Cambridge, 1995 (<a href="http://research.microsoft.com/~gmb/papers/thesis.pdf">pdf</a>)</p> </li> <li id="Benton95"> <p><a class='existingWikiWord' href='/nlab/show/Nick+Benton'>Nick Benton</a>, <em>A mixed linear and non-linear logic; proofs, terms and</em></p> <p>models_, In <em>Proceedings of Computer Science Logic</em> ‘94, vol. 933 of Lecture Notes in Computer Science. Verlag, June 1995.</p> </li> </ul> <p>Interpretation of this in <a class='existingWikiWord' href='/nlab/show/dependent+linear+type+theory'>dependent linear type theory</a> is in</p> <ul> <li id="PontoShulman12"><a class='existingWikiWord' href='/nlab/show/Kate+Ponto'>Kate Ponto</a>, <a class='existingWikiWord' href='/nlab/show/Mike+Shulman'>Mike Shulman</a>, <em>Duality and traces for indexed monoidal categories</em>, Theory and Applications of Categories, Vol. 26, 2012, No. 23, pp 582-659 (<a href="http://arxiv.org/abs/1211.1555">arXiv:1211.1555</a>)</li> </ul> <p>Further discussion of linear type theory is for instance in</p> <ul> <li> <p><em>Chapter 7, Linear type theory</em> <a href="http://www.cs.cmu.edu/~fp/courses/linear/handouts/lintt.pdf">pdf</a></p> </li> <li> <p>Anders Schack-Nielsen, Carsten Schürmann, <em>Linear contextual modal type theory</em> <a href="http://www.itu.dk/~carsten/papers/lcmtt.pdf">pdf</a></p> </li> <li> <p>Bernardo Toninho, Luís Caires, Frank Pfenning, <em>Dependent Session Types via Intuitionistic Linear Type Theory</em> <a href="http://ctp.di.fct.unl.pt/~lcaires/papers/dstypes.pdf">pdf</a></p> </li> <li> <p>Iliano Cervesato, <a class='existingWikiWord' href='/nlab/show/Frank+Pfenning'>Frank Pfenning</a>, <em>A Linear Logical Framework</em>, 1996, (<a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.1152">web</a>)</p> </li> </ul> <p>Discussion of application of linear logic to <a class='existingWikiWord' href='/nlab/show/quantum+logic'>quantum logic</a>, <a class='existingWikiWord' href='/nlab/show/quantum+computing'>quantum computing</a> and generally to <a class='existingWikiWord' href='/nlab/show/quantum+physics'>quantum physics</a> includes</p> <ul> <li> <p><a class='existingWikiWord' href='/nlab/show/Vaughan+Pratt'>Vaughan Pratt</a>, <em>Linear logic for generalized quantum mechanics</em>, in Proc. of <em>Workshop on Physics and Computation (PhysComp’92)</em> (<a href="http://boole.stanford.edu/pub/ql.pdf">pdf</a>, <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.137.7817">web</a>)</p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/Ross+Duncan'>Ross Duncan</a>, <em>Types for quantum mechanics</em>, 2006 (<a href="http://homepages.ulb.ac.be/~rduncan/papers/rduncan-thesis.pdf">pdf</a>)</p> </li> <li id="CCGP09"> <p>Gianpiero Cattaneo, Maria Luisa Dalla Chiara, Roberto Giuntini and Francesco Paoli, section 9 of <em>Quantum Logic and Nonclassical Logics</em>, p. 127 in Kurt Engesser, Dov M. Gabbay, Daniel Lehmann (eds.) <em>Handbook of Quantum Logic and Quantum Structures: Quantum Logic</em>, 2009 North Holland</p> </li> <li> <p><a class='existingWikiWord' href='/nlab/show/Ugo+Dal+Lago'>Ugo Dal Lago</a>, Claudia Faggian, <em>On Multiplicative Linear Logic, Modality and Quantum Circuits</em> (<a href="http://arxiv.org/abs/1210.0613">arXiv:1210.0613</a>)</p> </li> </ul> <p>Discussion of linear type theory without <a class='existingWikiWord' href='/nlab/show/units'>units</a> is in</p> <ul> <li><a class='existingWikiWord' href='/nlab/show/Robin+Houston'>Robin Houston</a>, <em>Linear Logic without Units</em> (<a href="http://arxiv.org/abs/1305.2231">arXiv:1305.2231</a>)</li> </ul> <p>Discussion of <a class='existingWikiWord' href='/nlab/show/inductive+types'>inductive types</a> in the context of linear type theory is in</p> <ul> <li>Stéphane Gimenez, <em>Towards Generic Inductive Constructions in Systems of Nets</em> (<a href="http://www.imn.htwk-leipzig.de/WST2013/papers/paper_16.pdf">pdf</a>)</li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on November 13, 2015 at 08:10:37. See the <a href="https://ncatlab.org/nlab/history/linear type theory" style="color: #005c19">history</a> of this page for a list of all contributions to it. </p> </div> <div class="navigation navfoot"> <a href="/nlab/edit/linear+type+theory" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a> | <a href="/nlab/revision/linear+type+theory/42" accesskey="B" class="navlink" id="to_previous_revision" rel="nofollow">Back in time</a> <span class='revisions'>(42 revisions)</span> | <a href="/nlab/show/diff/linear+type+theory" accesskey="C" class="navlink" id="see_changes" rel="nofollow">See changes</a> | <a href="/nlab/history/linear+type+theory" accesskey="S" class="navlink" id="history" rel="nofollow">History</a> | <a href="https://ncatlab.org/nlab/show/linear type theory/cite" style="color: black">Cite</a> <span class="views"> | Views: <a href="/nlab/print/linear+type+theory" accesskey="p" id="view_print" rel="nofollow">Print</a> | <a href="/nlab/tex/linear+type+theory" id="view_tex" rel="nofollow">TeX</a> | <a href="/nlab/source/linear+type+theory" id="view_source" rel="nofollow">Source</a> </span> </div> <div id="footer"> <div>This site is running on <a href="http://golem.ph.utexas.edu/instiki/show/HomePage">Instiki 0.19.7(MML+)</a></div> <div>Powered by <a href="http://rubyonrails.com/">Ruby on Rails</a> 2.3.18</div> </div> </div> <!-- Content --> </div> <!-- Container --> </body> </html>