% Talk_CSL.tex

\documentclass[fleqn,a4]{seminar}

%\newif\ifpdf
%\ifx\pdfoutput\undefined
%   \pdffalse
%\else
%   \pdfoutput=1
%   \pdftrue
%\fi  

%\ifpdf
%  \usepackage[pdftex]{graphicx}
%  \pdfcompresslevel=9
%  \pdfpagewidth=11truein %297truemm % your milage may vary....
%  \pdfpageheight=8.5truein %210truemm
%  \pdfhorigin=1truein     % default value(?), but doesn't work without
%  \pdfvorigin=1truein     % default value(?), but doesn't work without
%\else
%  \usepackage{graphicx}
%\fi

\raggedslides[0mm]

\usepackage{a4}

\usepackage{proof}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{url}
\usepackage{cmll}
%\usepackage{MnSymbol}
\usepackage{graphicx}
\usepackage{bussproofs}
\usepackage[all]{xy}
\SelectTips{cm}{}                 % - Looks pretty
\usepackage{comment}
\usepackage{lscape}

\usepackage{color}
\definecolor{darkblue}{rgb}{0,0,.7}
\definecolor{paleblue}{cmyk}{0.1,0.1,0,0}
\definecolor{darkgreen}{rgb}{0,.5,0}
\definecolor{darkred}{cmyk}{0.0,1.0,1.0,0.3}
\definecolor{darkmagenta}{cmyk}{0.0,1.0,0.0,0.4}
\definecolor{darkyellow}{cmyk}{0.0,0.0,1.0,0.4}
\definecolor{paleyellow}{cmyk}{0.0,0.0,0.5,0}
\definecolor{orange}{cmyk}{0.1,0.5,1.0,0.0}

\usepackage{hyperref}
\hypersetup{pdfstartview=FitH}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% layout and style

\renewcommand{\familydefault}{phv}
\renewcommand{\ttdefault}{cmtt}
\renewcommand{\rmdefault}{ppl}
\renewcommand{\sfdefault}{phv}

\renewcommand{\slideparskip}{1.5ex plus .2ex minus .2ex}

\setlength{\topsep}{0cm}
\parskip=6pt plus2pt minus2pt
\parindent=0pt


\newpagestyle{clems}%  <<<<<<<<<<<<<<<<<<<<<<<<<<<<<
  {}{\tcb{\emph{Annotation-Free Sequent Calculi for FILL \hfil \thepage}}}
\pagestyle{clems}

\slideframe{none}
\centerslidesfalse

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\definecolor{dkblue}{rgb}{0,0,.7}
\definecolor{dkgreen}{rgb}{0,.5,0}
\definecolor{greyout}{rgb}{0.7,0.7,0.7}
\newcommand\tc[2]{\textcolor{#1}{#2}}
\newcommand\tcr[1]{\tc{darkred}{#1}}
\newcommand\tcg[1]{\tc{dkgreen}{#1}}
\newcommand\tcb[1]{\tc{dkblue}{#1}}
\newcommand\tcgy[1]{\tc{greyout}{#1}}
\newcommand\Tcr[1]{\tcr{\textbf{#1}}}
\newcommand\Tcg[1]{\tcg{\textbf{#1}}}
\newcommand\Tcb[1]{\tcb{\textbf{#1}}}



\newcommand\heading[1]{
\subsection*{\tcb{#1}}
}
\newcommand\subheading[1]{
\subsubsection*{\tcb{#1}}
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%
%% Local definitions.
%%

\renewcommand{\comment}[1]{}

\def\punit{\bot}
\def\tunit{\mathrm{I}}
%\def\sunit{\Phi}
\def\sunit{\cdot}
\def\limp{\multimap}
%\def\excl{\leftY}
\def\excl{{-\!\!\!<}}
\def\ltens{\otimes}
\def\merge{\bullet}

\def\seq{\Rightarrow}
%\def\seq{>}

\def\fill{\mathrm{FILL}}
\def\biill{\mathrm{BiILL}}
\def\biilldc{\mathrm{BiILL}{\scriptstyle dc}}
%\def\fbills{\mathrm{BiILL}^{sn}}
\def\biillsn{\mathrm{BiILL}{\scriptstyle sn}}
%\def\fbilld{\mathrm{BiILL}^{dn}}
\def\biilldn{\mathrm{BiILL}{\scriptstyle dn}}
\def\filldc{\mathrm{FILL}{\scriptstyle dc}}
%\def\filld{\mathrm{FILL}^{dn}}
\def\filldn{\mathrm{FILL}{\scriptstyle dn}}
\def\impl{\supset}
\def\dimpl{\subset}
\def\bang{!}
\def\qm{?}

\def\drp{\mathit{drp}}
\def\rp{\mathit{rp}}

\newcommand{\binop}{\heartsuit}

\newcommand \seqtodisp[1]{\ulcorner{#1}\urcorner}
\newcommand\disptoseq[1]{\llcorner{#1}\lrcorner}
\def\Pc{\mathcal{P}}
\def\Qc{\mathcal{Q}}
\def\Sc{\mathcal{S}}
\def\Tc{\mathcal{T}}
\def\Uc{\mathcal{U}}
\def\Vc{\mathcal{V}}
\def\Xc{\mathcal{X}}
\def\Yc{\mathcal{Y}}
\def\Zc{\mathcal{Z}}

\def\turn{\vdash}
%\newcommand{\comment}[1]{}

%\def\fill{FILL}
\def\ill{ILL}
\def\mill{MILL}
\def\bill{BILL}
%\def\biill{BiILL}
\def\jill{JILL}
\def\gill{GILL}
\def\dill{DILL}

\def\gnab{?}
\def\adcn{\wedge}
\def\addn{\vee}
\def\adim{\to}
\def\adtp{\top}
\def\adbt{\bot}
%\def\mldn{\parr}
\def\mldn{\oplus}
\def\parr{\mldn}
\def\mlcn{\otimes}
\def\mltp{\mathbf{1}}
\def\mlbt{\bot}
\def\mlim{\multimap}
\def\mlli{\multimap^{-1}}
\def\mlri{\multimap}
\def\mlrx{
       \mbox{\,\raisebox{0.14ex}{$\scriptstyle>$}\!\!\raisebox{0.14ex}{$\scriptstyle -$}\,}}
\def\mllx{\excl}
%\def\mllx{
%       \mbox{\,\raisebox{0.13ex}{$\scriptstyle-$}\!\!\raisebox{0.13ex}{$\scriptstyle <$}\,}}

\def\sequent{\vdash}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}

\centerslidestrue
\begin{slide}
\vspace*{\stretch{2}}

\begin{center}\Large
\textbf{\tcb{Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic}}
\end{center}

\vspace{\stretch{1}}

\begin{center}
\tcg{\underline{Ranald Clouston}, Jeremy Dawson, Rajeev Gor\'e, Alwen Tiu} \\[2ex]
Logic and Computation Group \\
Research School of Computer Science \\
The Australian National University \\[2ex]

22nd EACSL Annual Conference on Computer Science Logic \\ (CSL '13 Torino) \\
2 September 2013
\end{center}

\vspace{\stretch{1}}

\end{slide}
\centerslidesfalse
%===================================================================

\begin{slide}
  \heading{Sequent Calculus: Classical vs Intuitionistic}

  Gentzen's calculus \Tcg{LK} for \tcg{classical} propositional logic has
  (multi-)sets of formulae to the left and right of a `turnstile' $\turn$.

  Commas on the left are interpreted as $\land$; on the right as $\lor$.

  To restrict to \tcg{intuitionistic} logic we restrict the right of the
  turnstile to singletons; indeed we need only make this restriction to
  ($\supset R$):
  \[
  \AxiomC{$\Gamma, A \sequent B$}
  \LeftLabel{($\supset R_1$)}
  \UnaryInfC{$\Gamma \sequent A \supset B$}
  \DisplayProof
  \qquad\qquad
  \AxiomC{$\Gamma, A \sequent B, \Delta$}
  \LeftLabel{($\supset R_2$)}
  \UnaryInfC{$\Gamma \sequent A \supset B, \Delta$}
  \DisplayProof
  \]

  If we make the same restriction with respect to ($\mlim R$) to a two-sided
  sequent calculus for (multiplicative) \tcg{linear logic}, where comma on the
  left is $\otimes$ and right is $\parr$, do we get a sensible logic?

\end{slide}

\begin{slide}
  \heading{The Schellinx calculus}

  [Schellinx 1991] posed this question and answered it in the negative -- such a
  calculus is \Tcg{not cut-free}:
  \[
  \AxiomC{$\vdots$}
  \UnaryInfC{$p\mlim q\turn p\mlim q$}
  \AxiomC{$\vdots$}
  \UnaryInfC{$r\parr s\turn r,s$}
  \BinaryInfC{$(p\mlim q)\parr(r\parr s)\turn \tcr{(p\mlim q)\parr r},s$}
  \AxiomC{$\vdots$}
  \UnaryInfC{$p\mlim q,p\turn q$}
  \AxiomC{$\vdots$}
  \UnaryInfC{$r\turn r$}
  \BinaryInfC{$(p\mlim q)\parr r,p\turn q\parr r$}
  \UnaryInfC{$\tcr{(p\mlim q)\parr r}\turn p\limp(q\parr r)$}
  \BinaryInfC{$(p\mlim q)\parr(r\parr s)\turn p\limp(q\parr r),s$}
  \DisplayProof
  \]
  This sequent cannot be proved without cut in the `Schellinx calculus'.

  Perhaps this argues for the usual absence of $\parr$ in
  intuitionistic linear logic - when we go classical, we get it `for free' via
  de Morgan duality.

  But is hope really lost for this logic?

%  [Hyland \& de Paiva 1993] asked two questions about this system:
%  \begin{enumerate}
%  \item Can an equivalent cut-free sequent sequent calculus be given?
%  \item What are the semantics of this logic?
%  \end{enumerate}

\end{slide}

\begin{slide}
  \heading{Full Intuitionistic Linear Logic -- Semantics}

  [Hyland \& de Paiva 1993] coined the name \tcg{Full Intuitionistic Linear
  Logic (FILL)} for the logic specified by the Schellinx calculus with cut, and
  gave its semantics in the category theoretic style:

  \begin{itemize}
  \item
    $(\otimes,I,\limp)$ is a \tcg{symmetric monoidal closed structure} (as
    usual);
  \item
    $(\parr,\bot)$ is a \tcg{symmetric monoidal structure};
  \item
    Interaction between these structures is entirely described by \tcg{weak
    distributivity}:
    $$
      A\otimes (B\parr C) \quad\to\quad (A\otimes B)\parr C
    $$
  \end{itemize}

  Semantics are great, but what we really want is a cut-free calculus...
%  Weak distributivity is equivalent to
%  $$
%    (p\limp q)\parr r \quad\to\quad p\limp(q\parr r)
%  $$
%  We call this \tcg{Grishin (b)}. Adding its converse Grishin (a) to FILL
%  recovers classical linear logic.

\end{slide}

\begin{slide}
  \heading{Full Intuitionistic Linear Logic -- Sequent Calculus}

  We need a `compromise' between the too-weak ($\mlim R_1$) and too-strong
  ($\mlim R_2)$:
  \[
  \AxiomC{$\Gamma, A \sequent B$}
  \LeftLabel{($\mlim R_1$)}
  \UnaryInfC{$\Gamma \sequent A \mlim B$}
  \DisplayProof
  \qquad\qquad
  \AxiomC{$\Gamma, A \sequent B, \Delta$}
  \LeftLabel{($\mlim R_2$)}
  \UnaryInfC{$\Gamma \sequent A \mlim B, \Delta$}
  \DisplayProof
  \]
  [Hyland \& de Paiva 1993] found this compromise by \tcg{annotating} their
  proofs via a term calculus, and then blocking ($\mlim R_2$) unless the
  variable for $A$ is not free for the terms for $\Delta$.
  
  The development is fiddly and, it turns out, wrong - [Bierman 1996] showed
  some cuts were still essential and offered two possible fixes (one due to
  Bellin). [Br\"{a}uner and de Paiva 1997] suggested another.

  All three fixes use the same strategy of using annotations to block invalid
  use of ($\mlim R_2$).

\end{slide}

\begin{slide}
  \heading{Our Example Again}

  \[
  \AxiomC{$\vdots$}
  \UnaryInfC{$p\mlim q,p\turn q$}
  \AxiomC{$\vdots$}
  \UnaryInfC{$r\parr s\turn r,s$}
  \BinaryInfC{$(p\mlim q)\parr(r\parr s),p\turn q,r,s$}
  \UnaryInfC{$(p\mlim q)\parr(r\parr s),\tcr{p}\turn q\parr r,\tcr{s}$}
  \UnaryInfC{$(p\mlim q)\parr(r\parr s)\turn p\limp(q\parr r),s$}
  \DisplayProof
  \]

  The bottom step is legal because our annotations confirm that $p$ is
  `independent' from $s$.

  It has been generally asserted in the literature that FILL
  \emph{requires} annotations for cut-free sequent calculus. This has seen it
  described as ``curious'', and even that it ``does not have a satisfactory
  proof theory''

  Our contribution is to show that such annotations are \Tcg{not} necessary.

\end{slide}

\begin{slide}
  \heading{Our Strategy}

  \begin{itemize}
    \item
    Give a \Tcg{display calculus} for FILL.
    \begin{description}
      \item[$\tcg{\checkmark}$]
      Easily shown to be complete.
      \item[$\tcg{\checkmark}$]
      Easily shown to support a cut-elimination procedure.
      \item[\mbox{\tcr{X}}]
      Embeds FILL into a bigger logic -- conservativity, and hence
      soundness, not clear.
      \item[\mbox{\tcr{X}}]
      Not well suited to proof search.
    \end{description}
    \item
    Refine display calculus to a \Tcg{nested sequent calculus} with \Tcg{deep
    inference}.
    \begin{description}
      \item[$\tcg{\checkmark}$]
      Conservativity, and hence soundness, now clear.
      \item[$\tcg{\checkmark}$]
      Supports proof search, shows that tautology problem for FILL is
      NP-complete.
    \end{description}
  \end{itemize}

\end{slide}

\begin{slide}
  \heading{Display calculus}

  \Tcg{Display calculus} [Belnap 1982] is an organising principle for sequent
  calculus that offers a generic cut-elimination procedure `for free'.

  Every \tcg{logical} connective has a \tcg{structural} counterpart: just as
  $\otimes$ and $\parr$ correlate to comma (depending on their position),
  $\limp$ correlates to $>$:
  \[
    \AxiomC{$X\turn A$}
    \AxiomC{$B\turn Y$}
    \LeftLabel{($\limp\turn$)\,}
    \BinaryInfC{$A\limp B\turn X>Y$}
    \DisplayProof
    \qquad\qquad
    \AxiomC{$X\turn A>B$}
    \LeftLabel{($\turn\limp$)\,}
    \UnaryInfC{$X\turn A\limp B$}
    \DisplayProof
  \]

  Any substructure can be \tcg{displayed} by applying residuation rules e.g.
  \[
    \AxiomC{$X,Y\turn Z$}
    \doubleLine
    \LeftLabel{(rp)\,}
    \UnaryInfC{$X\turn Y>Z$}
    \DisplayProof
    \qquad\qquad
    \AxiomC{$X, Y \turn Z$}
    \doubleLine
    \LeftLabel{(rp)\,}
    \UnaryInfC{$Y\turn X>Z$}
    \DisplayProof
  \]

  This \tcg{display property} is the heart of the cut-elimination theorem.

\end{slide}

\begin{slide}
  \heading{Display property - Comma on the right}

  We have seen how we deconstruct comma on the left ($\otimes$ in disguise)
  with (rp). What about comma on the right ($\parr$ in disguise)?

  \Tcg{Solution:} a new structural connective, $<$, and dual residuation
  rules:
  \[
    \AxiomC{$X\turn Y,Z$}
    \doubleLine
    \LeftLabel{(drp)\,}
    \UnaryInfC{$X<Y\turn Z$}
    \DisplayProof
    \qquad\qquad
    \AxiomC{$X \turn Y,Z$}
    \doubleLine
    \LeftLabel{(drp)\,}
    \UnaryInfC{$X<Z\turn Y$}
    \DisplayProof
  \]

  What \emph{is} this new structural connective?

  For now, view it as a meaningless syntactic tool, but observe that it raises
  immediate questions about \tcg{soundness}, as $X<Y\turn Z$ has no obvious
  meaning in FILL's semantics.

\end{slide}

\begin{slide}
  \heading{From Weak Distributivity to Grishin (b)}

  FILL's signature property, weak distributivity
  $$
    p\otimes (q\parr r) \quad\to\quad (p\otimes q)\parr r
  $$
  turns out to be equivalent to (either of) the \tcg{Grishin (b)} rules
  \[
    \AxiomC{$W,(X<Y)\turn Z$}
    \LeftLabel{(Grnb $\turn$)}
    \UnaryInfC{$(W,X)<Y\turn Z$}
    \DisplayProof
    \qquad
    \AxiomC{$W\vdash (X> Y), Z$}
    \LeftLabel{($\turn$ Grnb)}
    \UnaryInfC{$W\vdash X>(Y,Z)$}
    \DisplayProof
  \]

  If we had the \emph{converse} of these rules (\tcg{Grishin (a)}), we
  could `gather up' $Z$ with $Y$ to make $>$ (structural $\limp$) the
  main connective.

  We would hence effectively have an unrestrained ($\limp R$) rule, regaining
  classical linear logic exactly.

\end{slide}

\begin{slide}
  \heading{An Example Proof}

  \[
  \AxiomC{\tcgy{$\vdots$}}
  \UnaryInfC{\tcgy{$p\mlim q \turn p>q$}}
  \AxiomC{\tcgy{$\vdots$}}
  \UnaryInfC{\tcgy{$r\parr s\turn r,s$}}
  \BinaryInfC{\tcgy{$(p\mlim q)\parr(r\parr s)\turn (p>q),r,s$}}
  \UnaryInfC{\tcgy{$(p\mlim q)\parr(r\parr s)<s\turn (p>q),r$}}
  \UnaryInfC{\tcgy{$(p\mlim q)\parr(r\parr s)<s\turn p>(q,r)$}}
  \UnaryInfC{\tcgy{$((p\mlim q)\parr(r\parr s)<s),p\turn q,r$}}
  \UnaryInfC{\tcgy{$((p\mlim q)\parr(r\parr s)<s),p\turn q\parr r$}}
  \UnaryInfC{\tcgy{$(p\mlim q)\parr(r\parr s)<s\turn p> q\parr r$}}
  \UnaryInfC{$(p\mlim q)\parr(r\parr s)<s\turn p\limp(q\parr r)$}
  \UnaryInfC{$(p\mlim q)\parr(r\parr s)\turn p\limp(q\parr r),s$}
  \DisplayProof
  \]

\end{slide}

\begin{slide}
  \heading{An Example Proof}

  \[
  \AxiomC{\tcgy{$\vdots$}}
  \UnaryInfC{\tcgy{$p\mlim q \turn p>q$}}
  \AxiomC{\tcgy{$\vdots$}}
  \UnaryInfC{\tcgy{$r\parr s\turn r,s$}}
  \BinaryInfC{\tcgy{$(p\mlim q)\parr(r\parr s)\turn (p>q),r,s$}}
  \UnaryInfC{\tcgy{$(p\mlim q)\parr(r\parr s)<s\turn (p>q),r$}}
  \UnaryInfC{$(p\mlim q)\parr(r\parr s)<s\turn p>(q,r)$}
  \UnaryInfC{$((p\mlim q)\parr(r\parr s)<s),p\turn q,r$}
  \UnaryInfC{$((p\mlim q)\parr(r\parr s)<s),p\turn q\parr r$}
  \UnaryInfC{$(p\mlim q)\parr(r\parr s)<s\turn p> q\parr r$}
  \UnaryInfC{$(p\mlim q)\parr(r\parr s)<s\turn p\limp(q\parr r)$}
  \UnaryInfC{$(p\mlim q)\parr(r\parr s)\turn p\limp(q\parr r),s$}
  \DisplayProof
  \]

\end{slide}

\begin{slide}
  \heading{An Example Proof}

  \[
  \AxiomC{$\vdots$}
  \UnaryInfC{$p\mlim q \turn p>q$}
  \AxiomC{$\vdots$}
  \UnaryInfC{$r\parr s\turn r,s$}
  \BinaryInfC{$(p\mlim q)\parr(r\parr s)\turn (p>q),r,s$}
  \UnaryInfC{$(p\mlim q)\parr(r\parr s)<s\turn (p>q),r$}
  \UnaryInfC{$(p\mlim q)\parr(r\parr s)<s\turn p>(q,r)$}
  \UnaryInfC{$((p\mlim q)\parr(r\parr s)<s),p\turn q,r$}
  \UnaryInfC{$((p\mlim q)\parr(r\parr s)<s),p\turn q\parr r$}
  \UnaryInfC{$(p\mlim q)\parr(r\parr s)<s\turn p> q\parr r$}
  \UnaryInfC{$(p\mlim q)\parr(r\parr s)<s\turn p\limp(q\parr r)$}
  \UnaryInfC{$(p\mlim q)\parr(r\parr s)\turn p\limp(q\parr r),s$}
  \DisplayProof
  \]

  Note how $<$ was useful to `move $s$ out the way'.

  We will return to this theme of `deep inference'...

\end{slide}

\begin{slide}
  \heading{The Meaning of $<$ -- Exclusion}

  We may view $<$ as the structural version of a new logical connective
  $\excl$, called \tcg{exclusion} (sometimes \tcg{subtraction}):
  \[
  \AxiomC{$A<B\turn X$}
    \LeftLabel{($\excl\turn$)\,}
  \UnaryInfC{$A\excl B\turn X$}
  \DisplayProof
  \qquad\qquad
  \AxiomC{$X\turn A$}
  \AxiomC{$B\turn Y$}
  \LeftLabel{($\turn\excl$)\,}
  \BinaryInfC{$X<Y\turn A\excl B$}
  \DisplayProof
  \]

  A categorical semantics for FILL with this connective equips $\parr$ with
  a \tcg{co-closure}: a (natural) isomorphism between arrows
  $$
    A \;\to\; B\parr C \quad\mbox{and}\quad A\excl B \;\to\; C
  $$
  Call the corresponding logic \tcg{Bi-Intuitionistic Linear Logic (BiILL)}.

  Our display calculus is easily cut-free complete for FILL and BiILL, and
  sound for BiILL. FILL-soundness then reduces to the question of the
  \tcg{conservativity} of BiILL over FILL.

\end{slide}

\begin{slide}
  \heading{Nested sequents}

  We will refine our display calculus to a \tcg{deep inference} calculus with
  no structural rules (and hence no need for the troublesome (drp)).

  A convenient notation for this are \tcg{nested sequents}:
  $$
  S~~T \;::=\; S_1,\dots,S_k,A_1,\dots,A_m \seq B_1,\dots, B_n, T_1, \dots,T_l
  $$
  where $A_i$ and $B_j$ are formulae.

  This is a trivial variation on display calculus notation -- merely replace all
  $\turn,<,>$ with $\seq$.

  (To go back, we need to pay attention to whether a given $\seq$ appears on the
  left or right, and replace it with $<$ or $>$ as appropriate.)

\end{slide}

\begin{slide}
  \heading{Deep Inference and Merging}

  All proof rules can be applied \tcg{deeply} (in context).

  Many rules involve \tcg{merging} sequents -- nested sequents with the same
  tree structure merge by combining their formulae.

  Examples:
  $$
    \infer[\parr_l^d]
      {X[\Sc, A \parr B \seq \Tc]}
      {
        X_1[\Sc_1, A \seq \Tc_1]
        &
        X_2[\Sc_2, B \seq \Tc_2]
      }
   \qquad
   \infer[\parr_r^d]
     {X[\Sc \seq A \parr B, \Tc]}
     {X[\Sc \seq A, B, \Tc]}
  $$
  On the left $\Sc$ is a merge of $\Sc_1,\Sc_2$; $\Tc$ of $\Tc_1,\Tc_2$; $X[~]$
  of $X_1[~],X_2[~]$.

  $\parr_l^d$ is valid by weak distributivity.

\end{slide}

\begin{slide}
  \heading{Propagation}

  Along with rules for logical connectives and identity,
  \tcg{propagation} rules allow formulae to be moved levels in the nested
  sequents:

  $$
    \infer[pl_1]
    {X[\Sc, A \seq (\Sc' \seq \Tc'), \Tc]}
    {
    X[\Sc \seq (A, \Sc' \seq \Tc'), \Tc]
    }
    \qquad
    \infer[pr_1]
    {X[(\Sc \seq \Tc), \Sc' \seq A, \Tc']}
    {X[(\Sc \seq \Tc, A), \Sc' \seq \Tc']}
  $$
  $$
    \infer[pl_2]
    {X[\Sc, (\Sc', A \seq \Tc') \seq \Tc]}
    {X[\Sc, A, (\Sc' \seq \Tc') \seq \Tc]}
    \qquad
    \infer[pr_2]
    {X[\Sc \seq \Tc, (\Sc' \seq \Tc', A)]}
    {X[\Sc \seq \Tc, A, (\Sc' \seq \Tc')]}
  $$

  Again weak distributivity is the key to the validity of these rules.

\end{slide}

\begin{slide}
  \heading{Deep Inference: An Example}

  \[
  \AxiomC{ \ }
  \UnaryInfC{\tcgy{$\sunit\seq(p\seq p)$}}
  \AxiomC{ \ }
  \UnaryInfC{\tcgy{$\sunit\seq(q\seq q)$}}
  \BinaryInfC{\tcgy{$\sunit\seq (p\mlim q,p\seq q)$}}
  \UnaryInfC{\tcgy{$p\mlim q\seq (p\seq q)$}}
  \AxiomC{ \ }
  \UnaryInfC{\tcgy{$r\seq r,(\sunit\seq\sunit)$}}
  \UnaryInfC{\tcgy{$r\seq(\sunit\seq r)$}}
  \AxiomC{ \ }
  \UnaryInfC{\tcgy{$s\seq(\sunit\seq\sunit),s$}}
  \BinaryInfC{\tcgy{$r\parr s\seq (\sunit\seq r),s$}}
  \BinaryInfC{$(p\mlim q)\parr(r\parr s)\seq (p\seq q,r),s$}
  \UnaryInfC{$(p\mlim q)\parr(r\parr s)\seq (p\seq q\parr r),s$}
  \UnaryInfC{$(p\mlim q)\parr(r\parr s)\seq p\limp(q\parr r),s$}
  \DisplayProof
  \]

\end{slide}

\begin{slide}
  \heading{Deep Inference: An Example}

  \[
  \AxiomC{ \ }
  \UnaryInfC{\tcgy{$\sunit\seq(p\seq p)$}}
  \AxiomC{ \ }
  \UnaryInfC{\tcgy{$\sunit\seq(q\seq q)$}}
  \BinaryInfC{\tcgy{$\sunit\seq (p\mlim q,p\seq q)$}}
  \UnaryInfC{$p\mlim q\seq (p\seq q)$}
  \AxiomC{ \ }
  \UnaryInfC{\tcgy{$r\seq r,(\sunit\seq\sunit)$}}
  \UnaryInfC{\tcgy{$r\seq(\sunit\seq r)$}}
  \AxiomC{ \ }
  \UnaryInfC{\tcgy{$s\seq(\sunit\seq\sunit),s$}}
  \BinaryInfC{$r\parr s\seq (\sunit\seq r),s$}
  \BinaryInfC{$(p\mlim q)\parr(r\parr s)\seq (p\seq q,r),s$}
  \UnaryInfC{$(p\mlim q)\parr(r\parr s)\seq (p\seq q\parr r),s$}
  \UnaryInfC{$(p\mlim q)\parr(r\parr s)\seq p\limp(q\parr r),s$}
  \DisplayProof
  \]

\end{slide}

\begin{slide}
  \heading{Deep Inference: An Example}

  \[
  \AxiomC{ \ }
  \UnaryInfC{$\sunit\seq(p\seq p)$}
  \AxiomC{ \ }
  \UnaryInfC{$\sunit\seq(q\seq q)$}
  \BinaryInfC{$\sunit\seq (p\mlim q,p\seq q)$}
  \UnaryInfC{$p\mlim q\seq (p\seq q)$}
  \AxiomC{ \ }
  \UnaryInfC{$r\seq r,(\sunit\seq\sunit)$}
  \UnaryInfC{$r\seq(\sunit\seq r)$}
  \AxiomC{ \ }
  \UnaryInfC{$s\seq(\sunit\seq\sunit),s$}
  \BinaryInfC{$r\parr s\seq (\sunit\seq r),s$}
  \BinaryInfC{$(p\mlim q)\parr(r\parr s)\seq (p\seq q,r),s$}
  \UnaryInfC{$(p\mlim q)\parr(r\parr s)\seq (p\seq q\parr r),s$}
  \UnaryInfC{$(p\mlim q)\parr(r\parr s)\seq p\limp(q\parr r),s$}
  \DisplayProof
  \]

  Note that no $\seq$ on the left is introduced at any stage in this proof, so
  every sequent has a FILL translation (without $\excl$).

  This is a general property of the calculus (\tcg{separation}).

\end{slide}

\begin{slide}
  \heading{Theorems}

  \begin{description}
    \item[\tcg{Equivalence of Calculi}.] A formula is derivable in
      the display calculus iff it is derivable in the deep inference calculus.
      \begin{itemize}
        \item via an intermediate \tcg{shallow inference} nested sequent
          calculus.
      \end{itemize}
    \item[\tcg{Separation}.] The derivations of FILL formulae involve
      FILL-translatable sequents only.
    \item[\tcg{Soundness}.] The calculi are sound for FILL's semantics.
      \begin{itemize}
        \item by separation we need only check each nested rule on
          FILL-translatable sequents.
      \end{itemize}
    \item[\tcg{NP-completeness}.] \
      \begin{itemize}
        \item via encoding of Constants-Only multiplicative linear logic.
      \end{itemize}  
  \end{description}

\end{slide}

\begin{slide}
  \heading{Conclusion}

  FILL is (multiplicative) intuitionistic linear logic with $\parr$.

  Contrary to the literature, proof annotations are \Tcg{not}
  necessary for a cut-free sequent calculus.

  Instead use \tcg{display calculus} or \tcg{deep inference}.

  The former gives completeness, and cut elimination `for free', and its
  modularity makes FILL's relationship to other logics clear.

  The latter gives soundness and a complexity result.

  \Tcb{Future work}
  \begin{itemize}
    \item Extensions (exponentials, additives, MIX).
    \item Computational applications.
  \end{itemize}

\end{slide}

\end{document}

% LocalWords: intuitionistic Ranald Clouston Rajeev Gor Alwen Tiu nd EACSL CSL Torino LK multi Schellinx Hyland de Paiva monoidal Bierman Bellin uner conservativity Belnap residuation rp drp Grishin Grnb BiILL iff
