A Curry-Howard Correspondence for Intuitionistic Normal Modal Logic
スポンサーリンク
概要
- 論文の詳細を見る
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 call-by-name calculus is an extension of the simply typed call-by-name λ-calculus, and sound and complete for the categorical semantics. We show the strong normalizability and the confluency of the call-by-name calculus. On the other hand, the call-by-value calculus is an extension of the λc-calculus. We also show the strong normalizability and the confluency of the call-by-value one. This paper shows that a subcalculus of the call-by-value calculus is characterized by a CPS transformation into the call-by-name calculus. Moreover, we extend the call-by-name calculus to the modal logic IS4.
- 日本ソフトウェア科学会の論文
日本ソフトウェア科学会 | 論文
- LCDと透明弾性体の光弾性を用いたユーザインタフェース (特集 インタラクティブシステムとソフトウェア)
- Bluetoothによる位置検出
- COINSにおけるSIMD並列化(最新コンパイラ技術とCOINSによる実践)
- データ型を考慮した軽量なXML文書処理系の自動生成(ソフトウェア開発を支援する基盤技術)
- 計算と論理のための自然枠組NF/CAL(システム検証の科学技術)