Curry-Howard-Lambek Correspondence for Intuitionistic Belief

Cosimo Perini Brogi

This paper introduces a natural deduction calculus for intuitionistic logic of belief ${\mathsf{IEL}}^{-}$ which is easily turned into a modal $\lambda$-calculus giving a computational sem…