\begin{thebibliography}{10}

\bibitem{alechina:etal:01}
Natasha Alechina, Michael Mendler, Valeria de~Paiva, and Eike Ritter.
\newblock Categorical and {K}ripke semantics for constructive {S4} modal logic.
\newblock In L.~Fribourg, editor, {\em CSL'01}, volume 2142 of {\em
  LNCS}, pages 292--307. Springer, 2001.

\bibitem{bierman:paiva:00}
Gavin~M. Bierman and Valeria de~Paiva.
\newblock On an intuitionistic modal logic.
\newblock {\em Studia Logica}, 65(3):383--416, 2000.

\bibitem{brunnler:deepseq}
Kai Br{\"u}nnler.
\newblock Deep sequent systems for modal logic.
\newblock {\em Archive for Mathematical Logic}, 48(6):551--577, 2009.

\bibitem{bru:str:TABLEAUX09}
Kai Br{\"u}nnler and Lutz Stra{\ss}burger.
\newblock Modular sequent systems for modal logic.
\newblock In Martin Giese and Arild Waaler, editors, {\em  TABLEAUX'09}, volume 5607 of {\em
  Lecture Notes in Computer Science}, pages 152--166. Springer, 2009.

\bibitem{CGS:foccos}
Kaustuv Chaudhuri, Nicolas Guenot, and Lutz Stra{\ss}burger.
\newblock The focused calculus of structures.
\newblock In Marc Bezem, editor, {\em CSL'11}, volume~12 of {\em LIPIcs}, pages
  159--173. Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, 2011.

\bibitem{dyckhoff:92}
Roy Dyckhoff.
\newblock Contraction-free sequent calculi for intuitionistic logic.
\newblock {\em J. Symb. Log.}, 57(3):795--807, 1992.

\bibitem{ewald:86}
W.~B. Ewald.
\newblock Intuitionistic tense and modal logic.
\newblock {\em J. Symb. Log.}, 51, 1986.

\bibitem{fitch:48}
F.B. Fitch.
\newblock Intuitionistic modal logic with quantifiers.
\newblock {\em Portugaliae Mathematica}, 7(2):113--118, 1948.

\bibitem{fitting:nested-int}
Melvin Fitting.
\newblock Nested sequents for intuitionistic logic.
\newblock preprint, 2011.

\bibitem{fitting:label-nested}
Melvin Fitting.
\newblock Prefixed tableaus and nested sequents.
\newblock {\em Annals of Pure and Applied Logic}, 163:291--313, 2012.

\bibitem{galmiche:salhi:10}
Didier Galmiche and Yakoub Salhi.
\newblock Label-free natural deduction systems for intuitionistic and classical
  modal logics.
\newblock {\em Journal of Applied Non-Classical Logics}, 20(4):373--421, 2010.

\bibitem{garson:stanford}
Jim Garson.
\newblock Modal logic.
\newblock In Edward~N. Zalta, editor, {\em The Stanford Encyclopedia of
  Philosophy}. Stanford University, 2008.

\bibitem{gore:etal:aiml10}
Rajeev Gor{\'e}, Linda Postniece, and Alwen Tiu.
\newblock Cut-elimination and proof search for bi-intuitionistic tense logic.
\newblock In Valentin~Shehtman Lev~Beklemishev, Valentin~Goranko, editor, {\em
  Advances in Modal Logic}, pages 156--177. College Publications, 2010.

\bibitem{kashima:nested}
Ryo Kashima.
\newblock Cut-free sequent calculi for some tense logics.
\newblock {\em Studia Logica}, 53(1):119--136, 1994.

\bibitem{lamarche:contexts}
Fran\c{c}ois Lamarche.
\newblock On the algebra of structural contexts.
\newblock Accepted at \emph{Mathematical Structures in Computer Science}, 2001.

\bibitem{liang:07:csl}
Chuck Liang and Dale Miller.
\newblock Focusing and polarization in intuitionistic logic.
\newblock In J.~Duparc and T.~A. Henzinger, editors, {\em CSL 2007: Computer
  Science Logic}, volume 4646 of {\em LNCS}, pages 451--465. Springer-Verlag,
  2007.

\bibitem{mclaughlin:pfenning:FocIML}
Sean McLaughlin and Frank Pfenning.
\newblock The focused constraint inverse method for intuitionistic modal
  logics.
\newblock Draft manuscript, 2010.

\bibitem{mendler:scheele:11}
Michael Mendler and Stephan Scheele.
\newblock Cut-free gentzen calculus for multimodal ck.
\newblock {\em Inf. Comput.}, 209(12):1465--1490, 2011.

\bibitem{NPP:contextual}
Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka.
\newblock Contextual modal type theory.
\newblock {\em ACM Transactions on Computational Logic}, 9(3), 2008.

\bibitem{pfenning:davies:01}
Frank Pfenning and Rowan Davies.
\newblock A judgmental reconstruction of modal logic.
\newblock {\em Mathematical Structures in Computer Science}, 11(4):511--540,
  2001.

\bibitem{plotkin:stirling:86}
G.~D. Plotkin and C.~P. Stirling.
\newblock A framework for intuitionistic modal logic.
\newblock In J.~Y. Halpern, editor, {\em Theoretical Aspects of Reasoning About
  Knowledge}, 1986.

\bibitem{poggiolesi:tree}
Francesca Poggiolesi.
\newblock The method of tree-hypersequents for modal propositional logic.
\newblock In D.~Makinson, J.~Malinowski, and H.~Wansing, editors, {\em Towards
  Mathematical Philosophy}, volume~28 of {\em Trends in Logic}, pages 31--51.
  Springer, 2009.

\bibitem{prawitz:65}
Dag Prawitz.
\newblock {\em Natural Deduction, A Proof-Theoretical Study}.
\newblock Almquist and Wiksell, 1965.

\bibitem{fischer-servi:84}
G.~Fischer Servi.
\newblock Axiomatizations for some intuitionistic modal logics.
\newblock {\em Rend.\ Sem.\ Mat.\ Univers.\ Politecn.\ Torino}, 42(3):179--194,
  1984.

\bibitem{simpson:phd}
Alex Simpson.
\newblock {\em The Proof Theory and Semantics of Intuitionistic Modal Logic}.
\newblock PhD thesis, University of Edinburgh, 1994.

\end{thebibliography}