\begin{thebibliography}{10}

\bibitem{Belnap82JPL}
N.~D. Belnap.
\newblock Display logic.
\newblock {\em J. Philos. Logic}, 11:375--417, 1982.

\bibitem{Bierman:Note}
G.~M. Bierman.
\newblock A note on full intuitionistic linear logic.
\newblock {\em Ann. Pure Appl. Logic}, 79(3):281--287, 1996.

\bibitem{Brauner:Formulation}
T.~Br\"{a}uner and V.~de~Paiva.
\newblock A formulation of linear logic based on dependency-relations.
\newblock In {\em CSL}, pages 129--148, 1997.

\bibitem{Brunnler09AML}
K.~Br{\"u}nnler.
\newblock Deep sequent systems for modal logic.
\newblock {\em Arch. Math. Logic}, 48(6):551--577, 2009.

\bibitem{Clouston13CSL}
R.~Clouston, J.~E. Dawson, R.~Gor{\'e}, and A.~Tiu.
\newblock Annotation-free sequent calculi for full intuitionistic linear logic.
\newblock In {\em CSL}, pages 197--214, 2013.

\bibitem{ARXIV}
R.~Clouston, J.~E. Dawson, R.~Gor{\'e}, and A.~Tiu.
\newblock Annotation-free sequent calculi for full intuitionistic linear logic
  - extended version.
\newblock {\em CoRR}, abs/1307.0289, 2013.

\bibitem{DBLP:conf/tphol/DawsonG02}
J.~E. Dawson and R.~Gor{\'e}.
\newblock Formalised cut admissibility for display logic.
\newblock In {\em TPHOLs}, pages 131--147, 2002.

\bibitem{DBLP:conf/lpar/DawsonG10}
J.~E. Dawson and R.~Gor{\'e}.
\newblock Generic methods for formalising sequent calculi applied to
  provability logic.
\newblock In {\em LPAR}, pages 263--277, 2010.

\bibitem{Gore:SLD}
R.~Gor{\'e}.
\newblock Substructural logics on display.
\newblock {\em Log. J. IGPL}, 6(3):451--504, 1998.

\bibitem{Gore10AiML}
R.~Gor{\'e}, L.~Postniece, and A.~Tiu.
\newblock Cut-elimination and proof search for bi-intuitionistic tense logic.
\newblock In {\em AiML}, pages 156--177, 2010.

\bibitem{Gore11LMCS}
R.~Gor{\'e}, L.~Postniece, and A.~Tiu.
\newblock On the correspondence between display postulates and deep inference
  in nested sequent calculi for tense logics.
\newblock {\em LMCS}, 7(2), 2011.

\bibitem{Hyland:Full}
M.~Hyland and V.~de~Paiva.
\newblock Full intuitionistic linear logic (extended abstract).
\newblock {\em Ann. Pure Appl. Logic}, 64(3):273--291, 1993.

\bibitem{kashima-cut-free-tense}
R.~Kashima.
\newblock Cut-free sequent calculi for some tense logics.
\newblock {\em Studia Log.}, 53:119--135, 1994.

\bibitem{Park13}
J.~Park, J.~Seo, and S.~Park.
\newblock A theorem prover for boolean {BI}.
\newblock In {\em POPL}, pages 219--232, 2013.

\bibitem{poggiolesi-tree-hypersequents}
F.~Poggiolesi.
\newblock The method of tree-hypersequents for modal propositional logic.
\newblock In {\em Trends in Logic IV}, pages 31--51, 2009.

\bibitem{Schellinx:Some}
H.~Schellinx.
\newblock Some syntactical observations on linear logic.
\newblock {\em J. Logic Comput.}, 1(4):537--559, 1991.

\bibitem{Strassburger13}
L.~Stra{\ss}burger.
\newblock Cut elimination in nested sequents for intuitionistic modal logics.
\newblock In {\em FoSSaCS}, pages 209--224, 2013.

\bibitem{DBLP:conf/lics/TraytelPB12}
D.~Traytel, A.~Popescu, and J.~C. Blanchette.
\newblock Foundational, compositional (co)datatypes for higher-order logic:
  Category theory applied to theorem proving.
\newblock In {\em LICS}, pages 596--605, 2012.

\bibitem{Urban:Nominal}
C.~Urban.
\newblock Nominal techniques in isabelle/{HOL}.
\newblock {\em J. Automat. Reason.}, 40(4):327--356, 2008.

\end{thebibliography}
