N. Alechina, M. Mendler, E. Valeria-de-paiva, and . Ritter, Categorical and Kripke Semantics for Constructive S4 Modal Logic, LNCS, vol.2142, issue.01, pp.292-307, 2001.
DOI : 10.1007/3-540-44802-0_21

M. Gavin, V. Bierman, and . De-paiva, On an intuitionistic modal logic, Studia Logica, vol.65, issue.3, pp.383-416, 2000.

K. Brünnler, Deep sequent systems for modal logic, Archive for Mathematical Logic, vol.85, issue.2, pp.551-577, 2009.
DOI : 10.1007/s00153-009-0137-3

K. Brünnler and L. Straßburger, Modular Sequent Systems for Modal Logic, TABLEAUX'09, pp.152-166, 2009.
DOI : 10.1007/978-3-642-02716-1_12

K. Chaudhuri, N. Guenot, and L. Straßburger, The focused calculus of structures, Schloss Dagstuhl ? Leibniz-Zentrum fuer Informatik, pp.159-173, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00772420

R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic, The Journal of Symbolic Logic, vol.475, issue.03, pp.795-807, 1992.
DOI : 10.1007/3-540-54487-9_58

W. B. Ewald, Intuitionistic tense and modal logic, The Journal of Symbolic Logic, vol.344, issue.01, 1986.
DOI : 10.2307/2273953

F. B. Fitch, Intuitionistic modal logic with quantifiers, Portugaliae Mathematica, vol.7, issue.2, pp.113-118, 1948.

M. Fitting, Nested sequents for intuitionistic logic. preprint, 2011.

M. Fitting, Prefixed tableaus and nested sequents, Annals of Pure and Applied Logic, vol.163, issue.3, pp.291-313, 2012.
DOI : 10.1016/j.apal.2011.09.004

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.188.5887

D. Galmiche and Y. Salhi, Label-free natural deduction systems for intuitionistic and classical modal logics, Journal of Applied Non-Classical Logics, vol.18, issue.3, pp.373-421, 2010.
DOI : 10.1007/s10992-005-2267-3

URL : https://hal.archives-ouvertes.fr/hal-00580296

J. Garson, Modal logic, 2008.
DOI : 10.1017/CBO9781139856461.017

R. Goré, L. Postniece, and A. Tiu, Cut-elimination and proof search for bi-intuitionistic tense logic, Advances in Modal Logic, pp.156-177, 2010.

R. Kashima, Cut-free sequent calculi for some tense logics, Studia Logica, vol.13, issue.1, pp.119-136, 1994.
DOI : 10.1007/BF01053026

F. Lamarche, On the algebra of structural contexts, Accepted at Mathematical Structures in Computer Science, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00099461

C. Liang and D. Miller, Focusing and Polarization in Intuitionistic Logic, CSL 2007: Computer Science Logic, pp.451-465, 2007.
DOI : 10.1007/978-3-540-74915-8_34

URL : https://hal.archives-ouvertes.fr/inria-00167231

S. Mclaughlin and F. Pfenning, The focused constraint inverse method for intuitionistic modal logics, 2010.

M. Mendler and S. Scheele, Cut-free Gentzen calculus for multimodal <mml:math altimg="si1.gif" overflow="scroll" xmlns:xocs="http://www.elsevier.com/xml/xocs/dtd" xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns="http://www.elsevier.com/xml/ja/dtd" xmlns:ja="http://www.elsevier.com/xml/ja/dtd" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:tb="http://www.elsevier.com/xml/common/table/dtd" xmlns:sb="http://www.elsevier.com/xml/common/struct-bib/dtd" xmlns:ce="http://www.elsevier.com/xml/common/dtd" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:cals="http://www.elsevier.com/xml/common/cals/dtd"><mml:mi mathvariant="sans-serif">CK</mml:mi></mml:math>, Information and Computation, vol.209, issue.12, pp.1465-1490, 2011.
DOI : 10.1016/j.ic.2011.10.003

A. Nanevski, F. Pfenning, and B. Pientka, Contextual modal type theory, ACM Transactions on Computational Logic, vol.9, issue.3, 2008.
DOI : 10.1145/1352582.1352591

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1028.3796

F. Pfenning and R. Davies, A judgmental reconstruction of modal logic, Mathematical Structures in Computer Science, vol.11, issue.04, pp.511-540, 2001.
DOI : 10.1017/S0960129501003322

G. D. Plotkin and C. P. Stirling, A Framework for Intuitionistic Modal Logics, Theoretical Aspects of Reasoning About Knowledge, 1986.
DOI : 10.1016/B978-0-934613-04-0.50032-6

F. Poggiolesi, The Method of Tree-Hypersequents for??Modal??Propositional??Logic, Towards Mathematical Philosophy, pp.31-51, 2009.
DOI : 10.1007/978-1-4020-9084-4_3

URL : https://hal.archives-ouvertes.fr/halshs-00775815

D. Prawitz, Natural Deduction, A Proof-Theoretical Study. Almquist and Wiksell, 1965.

G. and F. Servi, Axiomatizations for some intuitionistic modal logics, Rend. Sem. Mat. Univers. Politecn. Torino, vol.42, issue.3, pp.179-194, 1984.

A. Simpson, The Proof Theory and Semantics of Intuitionistic Modal Logic, 1994.