Abstract The system of intuitionistic modal logic $\textbf{IEL}^{-}$ was proposed by S. Artemov and T. Protopopescu as the intuitionistic version of belief logic (S. Artemov and T. Protopopescu. Intuitionistic epistemic logic. The Review of Symbolic Logic, 9, 266–298, 2016). We construct the modal lambda calculus, which is Curry–Howard isomorphic to $\textbf{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 complete Kripke–Joyal-style semantics for predicate extensions of $\textbf{IEL}^{-}$ and related logics using Dedekind–MacNeille completions and modal cover systems introduced by Goldblatt (R. Goldblatt. Cover semantics for quantified lax logic. Journal of Logic and Computation, 21, 1035–1063, 2011). The paper extends the conference paper published in the LFCS’20 volume (D. Rogozin. Modal type theory based on the intuitionistic modal logic IEL. In International Symposium on Logical Foundations of Computer Science, pp. 236–248. Springer, 2020).