\documentclass{llncs}

\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{url}
\usepackage{cmll}
\usepackage[all]{xy}

% \usepackage{exptrees}

\newcommand\comment[1]{} 
\newcommand\biilldc{\mbox{BiILL}_{dc}}
\newcommand\filldc{\mbox{FILL}_{dc}}
\newcommand\biillsn{\mbox{BiILL}_{sn}}
\newcommand\fillsn{\mbox{FILL}_{sn}}
\newcommand\biilldn{\mbox{BiILL}_{dn}}
\newcommand\filldn{\mbox{FILL}_{dn}}

% \newcommand\biilldc{$\mbox{BiILL}_{dc}$}
% \newcommand\filldc{$\mbox{FILL}_{dc}$}
% \newcommand\biillsn{$\mbox{BiILL}_{sn}$}
% \newcommand\fillsn{$\mbox{FILL}_{sn}$}
% \newcommand\biilldn{$\mbox{BiILL}_{dn}$}
% \newcommand\filldn{$\mbox{FILL}_{dn}$}

\usepackage{proof}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{url}
% \usepackage{cmll}
%\usepackage{MnSymbol}
\usepackage{graphicx}
\usepackage{bussproofs}
\usepackage[all]{xy}
\usepackage{comment}
\usepackage{lscape}
\usepackage{color}

%\newcommand{\excl}{\mathrel{\rotatebox[origin=c]{180}{\ensuremath \multimap}}}

%\usepackage{txfonts}
%\usepackage{amsthm}

%\renewcommand{\labelenumi}{(\roman{enumi})}

\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{\tblue}[1]{\textcolor{blue}{#1}}
\newcommand{\tgreen}[1]{\textcolor{magenta}{#1}}
\newcommand{\tred}[1]{\textcolor{red}{#1}}
\newcommand{\TextRed}{\tred}

%\def\parr{\oplus}
%\def\punit{\bot}
\def\punit{\bot}
%\def\tunit{\mathrm{I}}
\def\tunit{\mltp}
%\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\ll{\mathrm{LL}}
\def\ill{\mathrm{ILL}}
\def\mill{\mathrm{MILL}}
\def\mall{\mathrm{MALL}}
\def\mll{\mathrm{MLL}}
\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]{}

\usepackage{color}
\definecolor{darkred}{cmyk}{0.0,1.0,1.0,0.3}
\newcommand\tc[2]{\textcolor{#1}{#2}}
\newcommand\tcr[1]{\tc{darkred}{#1}}

%%%%
%%%% Raj's defs. Need to be merged but want to chat with Ranald first
%%%%

%\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\mlcn{\otimes}
%\def\mltp{\mathbf{1}}
\def\mltp{\mathrm{I}}
\def\mlbt{\bot}
\def\mlze{\mathbf{0}}
%\def\mlze{0}
\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}

\newcommand{\imprightmc}{
 \AxiomC{$\Gamma, A \sequent B, \Delta$}
% \LeftLabel{$(\mlim R_1)$}
 \UnaryInfC{$\Gamma \sequent A \mlim B, \Delta$}
 \DisplayProof
}

\newcommand{\imprightsc}{
 \AxiomC{$\Gamma, A \sequent B$}
% \LeftLabel{$(\mlim R_1)$}
 \UnaryInfC{$\Gamma \sequent A \mlim B, \Delta$}
 \DisplayProof
}

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

%%
%\documentclass{llncs}
% \documentclass[a4paper,11pt]{article}
%\documentclass[twocolumn,a4paper,11pt]{article}

\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
%\usepackage{exptrees}
\usepackage{url}
\usepackage{bussproofs}

\renewcommand{\today}{\number\day\ 
  \ifcase\month\or
  January\or February\or March\or April\or May\or June\or
  July\or August\or September\or October\or November\or December\fi
  \ \number\year}

\setcounter{secnumdepth}2
\setcounter{tocdepth}2

% \newtheorem{theorem}{Theorem}[section]

\renewcommand{\qed}{\hfill$\dashv$}

% \newenvironment{proof}{
 % \noindent{\bf Proof:}}{\mbox{\bf Q.E.D.}\vspace{1ex}}

% \newtheorem{definition}{Definition}[section]

% \newtheorem{lemma}{Lemma}[section]

% \newtheorem{corollary}{Corollary}[section]
    
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Preamble

\newcommand\derl{\texttt{derl}}
\newcommand\derrec{\texttt{derrec}}
\newcommand\rls{\texttt{rls}}
\newcommand\adm{\texttt{adm}}

\newcommand\cfile{}

%\newcommand\comment[1]{} 
\newcommand\cc[1]{#1} % for label names 

\newcommand\invrule[2]{ 
% for use in non-math mode, args interpreted in math mode
  \begin{tabular}{@{}c@{}}
  $ #1 $ \\ \hline \hline $ #2 $
  \end{tabular}}
\newcommand\slrule[2]{ % similar to \frac, except
% for use in non-math mode, args interpreted in math mode
  \begin{tabular}{@{}c@{}}
  $ #1 $ \\ \hline $ #2 $
  \end{tabular}}

\renewcommand\theenumi{(\alph{enumi})}
\renewcommand\labelenumi{\theenumi}
\renewcommand\theenumii{(\roman{enumii})}
\renewcommand\labelenumii{\theenumii}

\newcommand\src[1]{source file \texttt{#1}}
\newcommand\apsrc[1]{Appendix \ref{app:code}}
\newcommand\seesrc[1]{(see source file \texttt{#1})}
\newcommand\insrc[1]{in source file \texttt{#1}}
\newcommand\page[1]{page~\pageref{#1}}
\newcommand\fig[1]{Fig.~\ref{fig:#1}}
\newcommand\ch[1]{Chapter~\ref{ch:#1}}
\newcommand\tbl[1]{Table~\ref{tbl:#1}}
\newcommand\thrm[1]{Theorem~\ref{thrm:#1}}
\newcommand\lem[1]{Lemma~\ref{lem:#1}}
\newcommand\ttl[1]{\tti{#1}\label{#1}}
\newcommand\ttdl[1]{\texttt{#1}\tti{#1}\label{#1}}
\newcommand\ttdef[1]{\texttt{#1}\tti{#1}}
\newcommand\tti[1]{\index{#1@\texttt{#1}}}
\newcommand\bfi[1]{\textbf{#1}\index{#1|textbf}}
\newcommand\dRA{{\boldmath $\delta$}\textbf{RA}}
\newcommand\dKt{{\boldmath $\delta$}\textbf{Kt}}
\newcommand\NRA{\textbf{NRA}}
\newcommand\RA{\textbf{RA}}
%\newcommand\M{$\mathcal M$}
\newcommand\MP{\ensuremath{\mathcal P}}
\newcommand\MQ{\ensuremath{\mathcal P}}
\newcommand\MR{\ensuremath{\mathcal C}}
\newcommand\M{\ensuremath{\mathcal M}}
\newcommand\Mp{$\mathcal M'$}
\newcommand\up[1]{\vspace{-#1ex}} 
\newcommand\vpf{\vspace{-3ex}} % to reduce space before proof tree
%\newcommand\1{\textbf 1}
\newcommand\0{\textbf 0}
\newcommand\cut{(\emph{cut})}
\newcommand\dt{\texttt{dt}}
\newcommand\dtn{\texttt{dtn}}

\newcommand{\pordered}[3]{#1 <_{\texttt{\scriptsize #2}} #3}
\newcommand{\Revpordered}[3]{#1 >_{\texttt{\scriptsize #2}} #3}
\newcommand{\LRPord}[2]{\pordered{#1}{LRP}{#2}}
\newcommand{\cutord}[2]{\pordered{#1}{cut}{#2}}
\newcommand{\snoneord}[2]{\pordered{#1}{sn1}{#2}}
\newcommand{\dtord}[2]{\pordered{#1}{dt}{#2}}
\newcommand{\Revdtord}[2]{\Revpordered{#1}{dt}{#2}}

\newcommand\GL{\textbf{GL}}
\newcommand\GLS{\textrm{GLS}}
\newcommand\GLR{\textit{GLR}}
\newcommand\GLRp{\ensuremath{\Box X, X, \Box B \vdash B}} % premise of GLR
\newcommand\GLRc{\ensuremath{\Box X \vdash \Box B}} % conclusion of GLR
\newcommand\lxxc{\ensuremath{\Box X, X \vdash B}} % conclusion of lem20
\newcommand\gbna{\ensuremath{\Box G, \Box B^k \vdash \Box A}} 
\newcommand\GLRB{\textit{GLR}($B$)}
\newcommand\GLRXB{\textit{GLR}($X,B$)}

\newcommand\pmz{\texttt{pm0}}
\newcommand\pmgez{\texttt{pm\_ge0}}

\newcommand\delz{\texttt{del0}}
\newcommand\delzs{\ensuremath{\partial^0}}

\newcommand\muxbn{\texttt{muxbn}}

\hyphenation{
 non-classical
 conn-ection
 typi-cally
 tradi-tional
 frame-works
 con-clusion
 deriv-ation
}

\pagestyle{plain}


\begin{document}

\title{From Categorical Semantics to Display Calculi to Deep Nested Sequent
  Calculi: Formalised for Full Intuitionistic Linear Logic}

\author{
Jeremy E.\ Dawson\inst{1}
 \and Ranald Clouston\inst{2}
 \and Rajeev Gor\'e\inst{1}
 \and Alwen Tiu\inst{3}}

\institute{
 Research School of Computer Science, Australian National University
\and  
 Department of Computer Science, Aarhus University
%% \and  
%%  Research School of Computer Science, Australian National University
\and 
School of Computer Engineering,  Nanyang Technological University}

\maketitle

\begin{abstract}

  Proof theory for a logic with categorical semantics can be developed
  by the following methodology: define a sound and complete display
  calculus for an extension of the logic with additional adjunctions;
  translate this calculus to a shallow inference nested sequent
  calculus; translate this calculus to a deep inference nested sequent
  calculus; then prove this final calculus is sound with respect to
  the original logic. This complex chain of translations between the
  different calculi require proofs that are technically intricate and
  involve a large number of cases, and hence are ideal candidates for
  formalisation.

  We present a formalisation of this methodology in the case of Full
  Intuitionistic Linear Logic (FILL), which is multiplicative
  intuitionistic linear logic extended with par. We discuss how our
  previous formalisations of display calculi and generalised
  derivability relations proved useful in this work, and 
  discuss the difficulties we encountered in formalising recursive
  data structures built out of multisets.

\end{abstract}

%\tableofcontents

\input{intro}
\input{general}
\input{dl}
\input{cats}
\input{eqcatsdl}
\input{shallow}
\input{eqdlshallow}
\input{deep}
\input{eqshallowdeep}
%\input{keep}
\input{soundness}
\input{related}
%\input{further}



\bibliographystyle{abbrv}
\bibliography{root}

%\input{apx}

\end{document}

% %%% Local Variables: 
% %%% mode: latex
% %%% TeX-master: t
% %%% End: 





