\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{BiILL}
%\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 
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.

\end{abstract}


\input{intro}
\input{general}
\input{cats}
\input{dl}
\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: 
