Curry-Howard-Lambek Correspondence for Intuitionistic Belief
This paper introduces a natural deduction calculus for intuitionistic logic of belief π¨π€π«^- which is easily turned into a modal Ξ»-calculus giving a computational semantics for deductions in π¨π€π«^-. By using that interpretation, it is also proved that π¨π€π«^- has good proof-theoretical properties. The correspondence between deductions and typed terms is then extended to a categorial semantics for identity of proofs in π¨π€π«^- showing the general structure of such a modality for belief in an intuitionistic framework.
READ FULL TEXT