Calculi for Intuitionistic Normal Modal Logic
Logic in Computer Science
2016-06-17 v1 Programming Languages
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.
Keywords
Cite
@article{arxiv.1606.03180,
title = {Calculi for Intuitionistic Normal Modal Logic},
author = {Yoshihiko Kakutani},
journal= {arXiv preprint arXiv:1606.03180},
year = {2016}
}