WEKO3
アイテム
Conservativity of Typed Lambda Calculus over Intuitionistic Logic
https://ipsj.ixsq.nii.ac.jp/records/118659
https://ipsj.ixsq.nii.ac.jp/records/1186596af8440c-3e64-483d-aa18-659d5ed0216e
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
KJ00001338276.pdf (162.0 kB)
|
|
| Item type | National Convention(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 1990-03-14 | |||||
| タイトル | ||||||
| 言語 | en | |||||
| タイトル | Conservativity of Typed Lambda Calculus over Intuitionistic Logic | |||||
| 言語 | ||||||
| 言語 | eng | |||||
| 資源タイプ | ||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||
| 資源タイプ | conference paper | |||||
| 著者所属 | ||||||
| 東北大 | ||||||
| 著者所属 | ||||||
| 東北大 | ||||||
| 著者所属 | ||||||
| 東北大 | ||||||
| 著者所属(英) | ||||||
| en | ||||||
| Research Institute of Electrical Communication, Tohoku University | ||||||
| 著者所属(英) | ||||||
| en | ||||||
| Research Institute of Electrical Communication, Tohoku University | ||||||
| 著者所属(英) | ||||||
| en | ||||||
| Research Institute of Electrical Communication, Tohoku University | ||||||
| 論文抄録(英) | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | 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. | |||||
| 書誌レコードID | ||||||
| 収録物識別子タイプ | NCID | |||||
| 収録物識別子 | AN00349328 | |||||
| 書誌情報 |
全国大会講演論文集 巻 第40回, 号 データ処理, p. 889-890, 発行日 1990-03-14 |
|||||
| 出版者 | ||||||
| 言語 | ja | |||||
| 出版者 | 情報処理学会 | |||||
