  Programming languages with algebraic effects often rely on effect annotations
to track algebraic operations in a computation. This is particularly important
in the presence of effect handlers, where handling of an effect may remove it
from the annotation in the computation's type.
  In this paper we view the algebraic effect theory of a computation as a
variable context, and track the effects directly in computation's modal type
with ECMTT, a novel calculus for algebraic effects and handlers. Our calculus
supports computations with effects and derives from Contextual Modal Type
Theory (CMTT), from which it inherits a number of important logical properties.
  In contrast to type-and-effect systems, where effects are attached as
annotations to a prior computational language, ECMMT tracks effects by a
contextualized variant of the modal $\Box$ (necessity) operator of the
intuitionistic modal logic of CMTT. In programming, the effect annotations are
explicitly managed by the dedicated term constructors corresponding to the
logical introduction and elimination forms for the modality. The modal
foundation leads to customary logical properties of local soundness and
completeness, and determines the operational semantics of ECMTT directly by
$\beta$-reduction. In addition, effect handlers become a generalization of
explicit substitutions, which in CMTT serve to reach one context from another.
  To the best of our knowledge, ECMTT is the first system to relate algebraic
effects to modal types. We also see it as a step towards providing a
correspondence in the style of Curry and Howard that may transfer a number of
results from the fields of modal logic and modal type theory to that of
algebraic effects.
