正規様相論理のためのCurry-Howard対応

• 角谷 良彦

  東京大学大学院情報理工学系研究科コンピュータ科学専攻

書誌事項

タイトル別名

• 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.

収録刊行物

• コンピュータ ソフトウェア

  コンピュータ ソフトウェア 25 (1), 167-179, 2008

  日本ソフトウェア科学会

詳細情報

• CRID: 1390001204736384384
• NII論文ID: 130004549096
• DOI: 10.11309/jssst.25.1_167
• ISSN: 02896540
• データソース種別:
  • JaLC
  • CiNii Articles
• 抄録ライセンスフラグ: 使用不可