linearlogic.toc

\contentsline {section}{\numberline {1}Introduction}{2}{section.1}
\contentsline {section}{\numberline {2}A sketch of linear logic proofs as algorithms}{3}{section.2}
\contentsline {section}{\numberline {3}Programs, algorithms and the $\lambda $-calculus}{5}{section.3}
\contentsline {section}{\numberline {4}Linear logic}{7}{section.4}
\contentsline {section}{\numberline {5}Semantics of linear logic}{13}{section.5}
\contentsline {subsection}{\numberline {5.1}Denotations of formulas}{14}{subsection.5.1}
\contentsline {subsection}{\numberline {5.2}Background on string diagrams and coalgebras}{15}{subsection.5.2}
\contentsline {subsection}{\numberline {5.3}The vector space semantics}{20}{subsection.5.3}
\contentsline {section}{\numberline {6}Cut-elimination}{24}{section.6}
\contentsline {subsection}{\numberline {6.1}An extended example}{27}{subsection.6.1}
\contentsline {section}{\numberline {7}Second-order linear logic}{29}{section.7}
\contentsline {section}{\numberline {A}Example of cut-elimination}{34}{appendix.A}
\contentsline {section}{\numberline {B}Tangents and proofs}{36}{appendix.B}