From applicative programming to verification-based knowledge: a Curry-Howard-Lambek reading

We discuss a modular natural deduction framework for intuitionistic modal logics dealing with applicative functors and verificationist knowledge, extending a calculus for belief/applicative programming (IEL⁻) to one (IEL) for knowledge in mathematics and other contexts as well. Through the proofs-as-programs paradigm, we map these systems into modal type theories and prove strong normalisation via CPS translations, uniformly handling detours and permutations. Finally, we give a categorical interpretation of the modal operator as a monoidal functor, reflecting the rewrite structure of the calculi.