  The system of intuitionistic modal logic ${\bf IEL}^{-}$ was proposed by S.
Artemov and T. Protopopescu as the intuitionistic version of belief logic
\cite{Artemov}. We construct the modal lambda calculus which is Curry-Howard
isomorphic to ${\bf IEL}^{-}$ as the type-theoretical representation of
applicative computation widely known in functional programming. We also provide
a categorical interpretation of this modal lambda calculus considering
coalgebras associated with a monoidal functor on a cartesian closed category.
  Finally, we study Heyting algebras and locales with corresponding operators.
Such operators are used in point-free topology as well. We study compelete
Kripke-Joyal-style semantics for predicate extensions of ${\bf IEL}^{-}$ and
related logics using Dedekind-MacNeille completions and modal cover systems
introduced by Goldblatt \cite{goldblatt2011cover}. The paper extends the
conference paper published in the LFCS'20 volume \cite{rogozin2020modal}.
