\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{linear type theory}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory}

[[!include type theory - contents]]

\hypertarget{monoidal_categories}{}\paragraph*{{Monoidal categories}}\label{monoidal_categories}

[[!include monoidal categories - contents]]

\hypertarget{linear_algebra}{}\paragraph*{{Linear algebra}}\label{linear_algebra}

[[!include homotopy - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{categorical_semantics}{Categorical semantics}\dotfill \pageref*{categorical_semantics} \linebreak
\noindent\hyperlink{the_canonical_comodality}{The canonical co-modality}\dotfill \pageref*{the_canonical_comodality} \linebreak
\noindent\hyperlink{HistoryCategoricalSemantics}{History of linear categorical semantics}\dotfill \pageref*{HistoryCategoricalSemantics} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak
\noindent\hyperlink{general}{General}\dotfill \pageref*{general} \linebreak
\noindent\hyperlink{lambeks_syntactic_calculus}{Lambek's syntactic calculus}\dotfill \pageref*{lambeks_syntactic_calculus} \linebreak
\noindent\hyperlink{categorical_semantics_2}{Categorical semantics}\dotfill \pageref*{categorical_semantics_2} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

\emph{Linear type theory} is the [[linear logic]]-version of [[type theory]]. In the definition of (\hyperlink{Seely89}{Seely 89, prop. 1.5}), following (\hyperlink{Girard87}{Girard 87}), this is the [[internal language]] of/has [[categorical semantics]] in [[star-autonomous categories]].

More generally, the term ``linear'' (as in \emph{linear type theory}) has over time come to connote [[internal languages|internal]] [[type theories]], and related logical frameworks ([[sequent calculus|sequent calculi]], [[natural deduction]]) that correspond to (usually symmetric) monoidal categories, where particularly the monoidal product is not assumed to be the cartesian product (reviews include \hyperlink{BlutePanangadenSeely94}{Blute-Panangaden-Seely 94}). Indeed, this general notion still faithfully follows the original motivation for the term ``linear'' as introduced in (\hyperlink{Girard87}{Girard 87}), since the non-cartesianness of the [[tensor product]] means the absence of a [[diagonal]] map and hence the impossibility of [[functions]] to depend on more than a single (linear) copy of their [[variables]].

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 [[star-autonomous categories]], one has languages for [[closed monoidal category|monoidal biclosed categories]], [[closed monoidal category|symmetric monoidal closed categories]], [[compact closed categories]], and others, collectively representing the ``multiplicative'' core of linear logic as understood in this general sense.

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).

Extending these considerations, the [[dependent type theory]]-version of linear type theory should be \emph{[[dependent linear type theory]]}.

Linear (dependent) type theory can be argued to be the proper [[type theory]] for [[quantum logic]]. In this context the linearity of the type theory, hence the absence of [[diagonal maps]] in its [[categorical semantics]], corresponds to the [[no-cloning theorem]] in [[quantum physics]].

\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

\hypertarget{categorical_semantics}{}\subsubsection*{{Categorical semantics}}\label{categorical_semantics}

(\ldots{})

In [[star-autonomous categories]].

\begin{tabular}{l|l|l}
Conjunctive operator&$\leftarrow$[[de Morgan duality]] $\rightarrow$&Disjunctive operator\\
\hline 
$\top$&&$0$\\
$1$&&$\bot$\\
$\&$&&$\oplus$\\
$\otimes$&&$\parr$\\
$^\bot$&&$^\bot$\\
$\bigwedge$&&$\bigvee$\\
$!$&&$?$\\
\end{tabular}

(\ldots{})

\hypertarget{the_canonical_comodality}{}\subsubsection*{{The canonical co-modality}}\label{the_canonical_comodality}

The original axiomatics for [[linear type theory]] in (\hyperlink{Girard87}{Girard 87}) contain in addition to the structures corresponding to a ([[star-autonomous category|star-autonomous]]) [[symmetric monoidal category|symmetric]] [[closed monoidal category]] a certain (co-)[[modality]] traditionally denoted ``$!$'', the [[exponential modality]]. In (\hyperlink{Benton95}{Benton 95}, \hyperlink{Bierman95}{Bierman 95}) it is noticed (reviewed in (\hyperlink{Barber97}{Barber 97, p. 21 (26)})) that a natural [[categorical semantics]] for this modality identifies it with the [[comonad]] that is induced from a [[strong monoidal adjunction]]

\begin{displaymath}
(\Sigma \dashv R)
  \;\colon\;
  \mathcal{C}
  \stackrel{\overset{\Sigma}{\leftarrow}}{\underset{R}{\longrightarrow}}
  S
\end{displaymath}
between the [[closed monoidal category|closed]] [[symmetric monoidal category]] $\mathcal{C}$ which interprets the given [[linear type theory]] and a [[cartesian monoidal category]] $S$.

If there is only the [[strong monoidal functor]] $\Sigma \;\colon\; S \longrightarrow \mathcal{C}$ without possibly a [[right adjoint]], then (\hyperlink{Barber97}{Barber 97, p. 21 (27)}) speaks of the \emph{structural [[fragment]]} of [[linear type theory]].

In (\hyperlink{PontoShulman12}{Ponto-Shulman 12}) it is observed that this in turn is canonically induced if $\mathcal{C} \simeq \mathcal{C}_\ast$ is the linear type theory over the trivial context of a [[dependent linear type theory]]/[[indexed closed monoidal category]] with category of contexts being $S$. See at \emph{\href{http://ncatlab.org/nlab/show/dependent+linear+type+theory#TheCanonicalComodality}{dependent linear type theory -- Properties -- Canonical co-modality}} for more on this.

\hypertarget{HistoryCategoricalSemantics}{}\subsection*{{History of linear categorical semantics}}\label{HistoryCategoricalSemantics}

There is a long history of logical frameworks of ``linear type'' and their categorical semantics in various [[doctrines]] 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.

The founding father could be said to be [[Joachim Lambek]], who was the first to apply deductive systems and particularly the method of Gentzen cut-elimination to what we would now recognize as [[categorification]]s of various [[fragments]] of propositional logic. It is noteworthy that one of the various first applications of this categorified cut-elimination was to the (\emph{linear}) doctrine of [[monoidal biclosed categories]], in which Lambek was interested in connection with his linguistic research (\hyperlink{Lambek58}{Lambek 58}); see (\hyperlink{Lambek68}{Lambek 68}, \hyperlink{Lambek69}{Lambek 69}). A principal goal in these papers was to study (and partially solve) the coherence problem for such structures.

\begin{remark}
\label{}\hypertarget{}{}
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 \hyperlink{KM71}{KM}. 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 \emph{is} made explicit).

\end{remark}
By the late 1970's, the connections between [[proof theory]], 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 [[fragments]] of classical logic, particularly in sequent calculus form, together with their categorical semantics, was collected in a book-length study (\hyperlink{Szabo78}{Szabo 78}) 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 \hyperlink{Jay90a}{Jay 90a}.)

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 \hyperlink{Minc77}{Minc 77}. This too was in view of coherence problems.

Interest in these problems was of course reawakened and reinvigorated in the light of Girard's extraordinarily insightful 1987 paper \hyperlink{Girard87}{Linear Logic}. The connection with closed symmetric monoidal categories and $\ast$-autonomous categories was picked up in very short order by the categorical community; an early account of this connection was given by \hyperlink{Seely89}{Seely 89}. It was not long before Girard's very fruitful exposition of linear proof theory and [[cut-elimination]] in terms of [[proof net|proof nets]], specifically for the [[multiplicative conjunction|multiplicative]] [[fragment]] 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).

These aspects are covered in (\hyperlink{Blute91}{Blute 91}), 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 [[fragments]] of MLL or doctrines of linear type.

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 (\hyperlink{Jay89}{Jay 89}, \hyperlink{Jay90b}{Jay 90b}). (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.)

\begin{remark}
\label{}\hypertarget{}{}
It should be noted that the ``classical'' techniques developed by Lambek, Kelly-Mac Lane, and Blute merely yield \emph{partial} 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 \emph{full} 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 $\ast$-autonomous categories, [[weakly distributive category|weakly distributive categories]], and full coherence thereof, see \hyperlink{BluteCockettSeelyTrimble96}{Blute-Cockett-Seely-Trimble96}.

\end{remark}
Meanwhile, the type theory and its categorical semantics for \emph{full} 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 \hyperlink{BentonBiermanPaivaHyland92}{Benton-Bierman-de Paiva-Hyland 92}, with an important antecedent in de Paiva's work on the Dialectica interpretation \hyperlink{dePaiva89}{de Paiva 89}. See also \hyperlink{HylandPaiva93}{Hyland-de Paiva 93}, \hyperlink{Bierman95}{Bierman 95}, \hyperlink{Barber97}{Barber 97}

See also \hyperlink{Schalk04}{Schalk 04}, \hyperlink{Mellies09}{Melli\`e{}s 09}. Schalk and Melli\`e{}s have also worked on game-theoretic semantics of theories of linear type -- which itself has a long and intricate history.

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.

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[propositions as projections]]


\item [[modal type theory]]


\item [[geometric homotopy type theory]]


\item [[stable homotopy type]]



\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

\hypertarget{general}{}\subsubsection*{{General}}\label{general}

The original article on [[linear logic]] is

\begin{itemize}%
\item [[Jean-Yves Girard]], \emph{Linear logic}, Theoretical Computer Science 50:1, 1987. (\href{http://iml.univ-mrs.fr/~girard/linear.pdf}{pdf})

\end{itemize}
A review of linear logic is in

\begin{itemize}%
\item [[Jean-Yves Girard]], part III of \emph{[[Lectures on Logic]]}, European Mathematical Society 2011

\end{itemize}
Linear type theory as such is made explicit for instance in

\begin{itemize}%
\item Masahito Hasegawa. \emph{Logical predicates for intuitionistic linear type theories}, Typed Lambda Calculi and Applications: 4th International Conference, TLCA `99, ed. J.-Y. Girard, Lecture Notes in Computer Science 1581, Springer, Berlin, 1999 (\href{http://www.kurims.kyoto-u.ac.jp/~hassei/papers/tlca99.pdf}{pdf})


\item \href{http://www.cs.cmu.edu/~fp/courses/15816-f01/handouts/lintt.pdf}{pdf}



\end{itemize}
\hypertarget{lambeks_syntactic_calculus}{}\subsubsection*{{Lambek's syntactic calculus}}\label{lambeks_syntactic_calculus}

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 [[categorial grammar]]):

\begin{itemize}%
\item [[Joachim Lambek]]. \emph{The mathematics of sentence structure} . American mathematical monthly, 154-170, 1958. \href{http://www.jstor.org/stable/2310058}{link}

\end{itemize}
Lambek called his system the ``syntactic calculus'', while nowadays it is often called \emph{Lambek calculus} in linguistics.

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 [[homological algebra]]:

\begin{quote}%
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'', \emph{Advances in Linear Logic}, CUP, 1995)


\end{quote}
\hypertarget{categorical_semantics_2}{}\subsubsection*{{Categorical semantics}}\label{categorical_semantics_2}

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.

\begin{itemize}%
\item [[Joachim Lambek]], \emph{Deductive systems and categories}, Mathematical Systems Theory 2 (1968), 287-318.


\item [[Joachim Lambek]], \emph{Deductive systems and categories II}, Lecture Notes in Math. 86, Springer-Verlag (1969), 76-122.


\item G.E. Minc, \emph{Closed categories and the theory of proofs}, 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, \emph{Selected Papers in Proof Theory}, Bibliopolis (1992).


\item M.E. Szabo, \emph{Algebra of Proofs}, Studies in Logic and the Foundations of Mathematics, vol. 88 (1978), North-Holland.


\item C.B. Jay, \emph{Languages for monoidal categories}, JPAA 59 (1989), 61-85.


\item C.B. Jay, \emph{Coherence in category theory and the Church-Rosser property}. Unpublished preprint (1990), cited in the following reference.


\item C.B. Jay, \emph{The structure of free closed categories}, JPAA 66 (1990), 271-285.



\end{itemize}
The [[categorical semantics]] of linear type theory in [[star-autonomous categories]] was first described in

\begin{itemize}%
\item [[R. A. G. Seely]], \emph{Linear logic, $\ast$-autonomous categories and cofree coalgebras}, \emph{Contemporary Mathematics} 92, 1989. ([[SeelyLinearLogic.pdf:file]], \href{http://www.math.mcgill.ca/rags/nets/llsac.ps.gz}{ps.gz})

\end{itemize}
with the first non-syntactic, mathematical categorical model in the same volume:

\begin{itemize}%
\item [[Valeria de Paiva]], \emph{The Dialectica Categories}, \emph{Contemporary Mathematics} 92, 1989. (\href{http://www.cs.bham.ac.uk/~vdp/publications/dial87.pdf}{web})

\end{itemize}
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

\begin{itemize}%
\item [[Richard Blute]], \emph{Linear logic, coherence, and dinaturality}, Dissertation, University of Pennsylvania 1991, published in Theoretical Computer Science archive Volume 115 Issue 1, (July 5, 1993) 3-41.

\end{itemize}
Blute's thesis derives coherence theorems for various doctrines of ``linear type'', including a coherence theorem for symmetric monoidal [[closed categories]] due to Kelly and Mac Lane:

\begin{itemize}%
\item [[Max Kelly]], [[Saunders MacLane]], \emph{Coherence in closed categories}, JPAA 1 (1971), 97-140 (\href{http://www.sciencedirect.com/science/article/pii/0022404971900132}{web})

\end{itemize}
An decent review of some of this is in

\begin{itemize}%
\item [[Richard Blute]], [[Prakash Panangaden]], [[R. A. G. Seely]], \emph{Fock Space: A Model of Linear Exponential Types} (1994) (\href{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.6825}{web})

\end{itemize}
Extensions of the coherence-theoretic applications of proof nets in Blute's thesis, to give full solutions to coherence problems, were given in

\begin{itemize}%
\item [[Todd Trimble]], \emph{Linear Logic, Bimodules, and Full Coherence for Autonomous Categories, Rutgers 1994}


\item [[Richard Blute]], Cockett, [[R. A. G. Seely]], [[Todd Trimble]], \emph{Natural deduction and coherence for weakly distributive categories}, JPAA 113 (1996), 229-296. (\href{http://www.sciencedirect.com/science/article/pii/002240499500159X}{web})



\end{itemize}
Type theory for full linear logic, together with its categorical interpretation, was developed in

\begin{itemize}%
\item [[Nick Benton]], Gavin Bierman, [[Valeria de Paiva]], [[Martin Hyland]], \emph{Term assignments for intuitionistic linear logic}. Technical report 262, Cambridge 1992 (\href{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.8666}{citeseer})


\item [[Martin Hyland]], [[Valeria de Paiva]], \emph{Full Intuitionistic Linear Logic} (extended abstract). Annals of Pure and Applied Logic, 64(3), pp.273-291, 1993. (\href{http://www.cs.bham.ac.uk/~vdp/publications/fill.pdf}{pdf})


\item Andrew Graham Barber, \emph{Linear Type Theories, Semantics and Action Calculi}, PhD Thesis, Edinburgh 1997 (\href{http://www.lfcs.inf.ed.ac.uk/reports/97/ECS-LFCS-97-371/&#8206;}{web}, \href{http://www.lfcs.inf.ed.ac.uk/reports/97/ECS-LFCS-97-371/ECS-LFCS-97-371.pdf}{pdf})



\end{itemize}
Further review and discussion is in

\begin{itemize}%
\item Gavin M. Bierman, \emph{What is a categorical model of intuitionistic linear logic? (\href{http://research.microsoft.com/en-us/um/people/gmb/papers/tlca95.pdf}{web})}

\end{itemize}
The more general case of general [[symmetric monoidal categories]] is reviewed and further discussed in

\begin{itemize}%
\item Andrea Schalk, \emph{What is a categorical model for linear logic?} (\href{http://www.cs.man.ac.uk/&#8764;schalk/notes/llmodel.pdf}{pdf})


\item [[Richard Blute]], Philip Scott, \emph{Category theory for linear logicians}, 2004 (\href{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.6250}{citeseer})


\item [[Paul-André Melliès]] , \emph{Categorial Semantics of Linear Logic}, in \emph{Interactive models of computation and program behaviour}, Panoramas et synth\`e{}ses 27, 2009 (\href{http://www.pps.univ-paris-diderot.fr/~mellies/papers/panorama.pdf}{pdf})



\end{itemize}
The interpretation of Girard's $!$-modality as the [[comonad]] induced from a [[monoidal adjunction]] between the closed [[symmetric monoidal category]] and a [[cartesian closed category]] is due to

\begin{itemize}%
\item G. Bierman, \emph{On Intuitionistic Linear Logic} PhD thesis, Computing Laboratory, University of Cambridge, 1995 (\href{http://research.microsoft.com/~gmb/papers/thesis.pdf}{pdf})


\item [[Nick Benton]], \emph{A mixed linear and non-linear logic; proofs, terms and models}, In \emph{Proceedings of Computer Science Logic} `94, vol. 933 of Lecture Notes in Computer Science. Verlag, June 1995.



\end{itemize}
Interpretation of this in [[dependent linear type theory]] is in

\begin{itemize}%
\item [[Kate Ponto]], [[Mike Shulman]], \emph{Duality and traces for indexed monoidal categories}, Theory and Applications of Categories, Vol. 26, 2012, No. 23, pp 582-659 (\href{http://arxiv.org/abs/1211.1555}{arXiv:1211.1555})

\end{itemize}
Further discussion of linear type theory is for instance in

\begin{itemize}%
\item \emph{Chapter 7, Linear type theory} \href{http://www.cs.cmu.edu/~fp/courses/linear/handouts/lintt.pdf}{pdf}


\item Anders Schack-Nielsen, Carsten Sch\"u{}rmann, \emph{Linear contextual modal type theory} \href{http://www.itu.dk/~carsten/papers/lcmtt.pdf}{pdf}


\item Bernardo Toninho, Lu\'i{}s Caires, Frank Pfenning, \emph{Dependent Session Types via Intuitionistic Linear Type Theory} \href{http://ctp.di.fct.unl.pt/~lcaires/papers/dstypes.pdf}{pdf}


\item Iliano Cervesato, [[Frank Pfenning]], \emph{A Linear Logical Framework}, 1996, (\href{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.1152}{web})



\end{itemize}
Discussion of application of linear logic to [[quantum logic]], [[quantum computing]] and generally to [[quantum physics]] includes

\begin{itemize}%
\item [[Vaughan Pratt]], \emph{Linear logic for generalized quantum mechanics}, in Proc. of \emph{Workshop on Physics and Computation (PhysComp'92)} (\href{http://boole.stanford.edu/pub/ql.pdf}{pdf}, \href{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.137.7817}{web})


\item [[Ross Duncan]], \emph{Types for quantum mechanics}, 2006 (\href{http://homepages.ulb.ac.be/~rduncan/papers/rduncan-thesis.pdf}{pdf})


\item Gianpiero Cattaneo, Maria Luisa Dalla Chiara, Roberto Giuntini and Francesco Paoli, section 9 of \emph{Quantum Logic and Nonclassical Logics}, p. 127 in Kurt Engesser, Dov M. Gabbay, Daniel Lehmann (eds.) \emph{Handbook of Quantum Logic and Quantum Structures: Quantum Logic}, 2009 North Holland


\item [[Ugo Dal Lago]], Claudia Faggian, \emph{On Multiplicative Linear Logic, Modality and Quantum Circuits} (\href{http://arxiv.org/abs/1210.0613}{arXiv:1210.0613})



\end{itemize}
Discussion of linear type theory without [[units]] is in

\begin{itemize}%
\item [[Robin Houston]], \emph{Linear Logic without Units} (\href{http://arxiv.org/abs/1305.2231}{arXiv:1305.2231})

\end{itemize}
Discussion of [[inductive types]] in the context of linear type theory is in

\begin{itemize}%
\item St\'e{}phane Gimenez, \emph{Towards Generic Inductive Constructions in Systems of Nets} (\href{http://www.imn.htwk-leipzig.de/WST2013/papers/paper_16.pdf}{pdf})

\end{itemize}
[[!redirects linear type theories]]

[[!redirects linear type]] [[!redirects linear types]]

[[!redirects linear homotopy type]] [[!redirects linear homotopy types]]

[[!redirects linear type]] [[!redirects linear types]]



\end{document}