Calculi for Intuitionistic Normal Modal Logic
classification
💻 cs.LO
cs.PL
keywords
calculuscalculicall-by-namecall-by-valueintuitionisticlogicmodalcompleteness
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.