Conservativity of Typed Lambda Calculus over Intuitionistic Logic

スポンサーリンク

概要

• 論文の詳細を見る

• We investigate the conservativity of typed λ-calculi placed in λ-cube over intuitionistic logical systems. Some of typed λ-calculi in λ-cube are well-known. It is already proved that using formulae-as-types notion, the interpretations from typed λ-calculi in λ-cube to intuitionistic logical systems are sound. Firstly we summarize already obtained results about the conservativity in 2. Secondly, in order to solve the open problem that λP2 is conservative over PRED2 (denoted 2nd-order int. predicate logic) or not, for a first trial, we will prove the reduced problem that λP2 is conservative over PRED2'(denoted PRED2 with (*_t, *_t)) in 3.

• 一般社団法人情報処理学会の論文
• 1990-03-14

著者

• 野口 正一

  東北大・電気通信研

• 藤田 憲悦

  東北大

• 富樫 敦

  東北大学 電気通信研究所

関連論文

• パネル討論会 : 新しい情報処理デバイスの展望 : 新しい計算機システム構築のために : 昭和59年後期第29回全国大会報告
• 情報処理技術の今後
• パネル討論会 : 創立30周年記念 : 日本における情報処理教育のあり方
• PC Communication in an OSI environment : TM&T : Mail and Talk on TAINS
• Graphical Interface for Representation of LTS
• PrologプログラムのAND-OR並列実行モデル
• Conservativity of Typed Lambda Calculus over Intuitionistic Logic
• Relationship Between Logic And Type System

スポンサーリンク