Curry–Howard–Lambek Correspondence for Intuitionistic Belief

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