Calculi for Intuitionistic Normal Modal Logic

Abstract

This paper provides a call-by-name and a call-by-value term calculus, both of which have a Curry-Howard correspondence to the box fragment of the intuitionistic modal logic IK. The strong normalizability and the confluency of the calculi are shown. Moreover, we define a CPS transformation from the call-by-value calculus to the call-by-name calculus, and show its soundness and completeness.

Cited by in corpus (7)

• Cut-Elimination and Proof Search for Bi-Intuitionistic Tense Logic
• The Many Worlds of Modal λ-calculi: I. Curry-Howard for Necessity, Possibility and Time
• Dual-Context Calculi for Modal Logic
• Modality via Iterated Enrichment
• Categorical and Algebraic Aspects of the Intuitionistic Modal Logic ${\mathrm{IEL}}^{-}$ and its predicate extensions
• An analytic calculus for intuitionistic belief
• Curry-Howard-Lambek Correspondence for Intuitionistic Belief