%
% \documentclass{llncs}

\documentclass[a4paper,UKenglish]{lipics}

% \usepackage[margin=1in]{geometry}

%\usepackage{microtype}%if unwanted, comment out or use option "draft"

\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}

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

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

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

\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]{}

\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\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}

\theoremstyle{plain}
\newtheorem{proposition}[theorem]{Proposition}

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

\title{Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic}
\author{Ranald Clouston}
\author{Jeremy Dawson}
\author{Rajeev Gor\'e}
\author{Alwen Tiu
%\thanks{We gratefully acknowledge the close reading and detailed questions of
%Jeremy Dawson.}
}
\affil{Logic and Computation Group, Research School of Computer Science,\\
The Australian National University, Canberra ACT 0200, Australia}
\authorrunning{R. Clouston, J. Dawson, R. Gor\'e, A. Tiu}
\Copyright{R. Clouston, J. Dawson, R. Gor\'e, A. Tiu}

\subjclass{F.4.1 Mathematical Logic}

\keywords{Linear logic, display calculus, nested sequent calculus, deep inference}

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

%Editor-only macros (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\serieslogo{}%please provide filename (without suffix)
\volumeinfo%(easychair interface)
  {Billy Editor, Bill Editors}% editors
  {2}% number of editors: 1, 2, ....
  {Conference title on which this volume is based on}% event
  {1}% volume
  {1}% issue
  {1}% starting page number
\EventShortName{}
\DOI{10.4230/LIPIcs.xxx.yyy.p}% to be completed by the volume editor
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}

\maketitle

\begin{abstract}
  Full Intuitionistic Linear Logic (FILL) is multiplicative
  intuitionistic linear logic extended with par. Its proof theory has
  been notoriously difficult to get right, and existing sequent
  calculi all involve inference rules with complex annotations to
  guarantee soundness and cut-elimination. We give a simple and
  annotation-free display calculus for FILL which satisfies Belnap's
  generic cut-elimination theorem. To do so, our display calculus
  actually handles an extension of FILL, called Bi-Intuitionistic
  Linear Logic (BiILL), with an `exclusion' connective defined via an
  adjunction with par. We refine our display calculus for BiILL into a
  cut-free nested sequent calculus with deep inference
%for BiILL
  in which the
%numerous
  explicit structural rules of the display calculus
  become admissible. A separation property guarantees that
%cut-free
  proofs of FILL formulae in the
%nested
  deep inference calculus
%introduce only connectives of FILL.
  contain no trace of exclusion.
  Each such rule is sound for the
  semantics of FILL, thus our
%nested deep sequent
  deep inference calculus and
%our
  display calculus are conservative over FILL. The
  deep inference calculus also enjoys the subformula property and
  terminating backward proof search, which gives the NP-completeness
  of BiILL and FILL.
\end{abstract}
% \begin{abstract}
% Full Intuitionistic Linear Logic (FILL) is multiplicative
% intuitionistic linear logic extended with par. Its proof theory has
% been notoriously difficult to get right, and existing sequent calculi
% all involve inference rules with complex annotations to guarantee
% soundness and cut-elimination. We give a simple annotation-free
% display calculus for FILL which satisfies Belnap's generic
% cut-elimination theorem. To do so, it is necessary to move to an
% extension of FILL, called Bi-Intuitionistic Linear Logic (BiILL), with
% an `exclusion' connective defined via an adjunction with par. We show
% that our display calculus is conservative over FILL via a novel
% sequent rewriting procedure. Since the structural rules of display
% calculi are bad for proof search, we show how they can be absorbed by
% refining our calculus to a cut-free nested sequent calculus with deep
% inference. Our resulting deep-inference calculus enjoys a separation
% property, which allows us to obtain complete fragments of BiILL,
% including FILL. It also enjoys the subformula property, which enables
% terminating backward proof-search and allows us to prove the
% NP-completeness of BiILL and FILL.
% \end{abstract}


\input{intro}

\input{display}
%\input{biill_to_fill}

\input{shallow}
\input{deep}
\input{equiv}
\input{conserv}

\input{concl}

%\vspace*{-1em}
\bibliographystyle{abbrv}
\bibliography{biblio}

\newpage
\appendix
\input{apx}

%\newpage
%\input{junk}
\end{document}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "root"
%%% End: 
