Curry-Howard-Lambek Correspondence for Intuitionistic Belief

This paper introduces a natural deduction calculus for intuitionistic logic of belief ${\mathsf{I}\mathsf{E}\mathsf{L}}^{-}$ which is easily turned into a modal $\lambda$-calculus giving a computational semantics for deductions in ${\mathsf{I}\mathsf{E}\mathsf{L}}^{-}$. By using that interpretation, it is also proved that ${\mathsf{I}\mathsf{E}\mathsf{L}}^{-}$ has good proof-theoretic properties. The correspondence between deductions and typed terms is then extended to a categorical semantics for identity of proofs in ${\mathsf{I}\mathsf{E}\mathsf{L}}^{-}$ showing the general structure of such a modality for belief in an intuitionistic framework.