| 研究課題/領域番号 |
23500030
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎
|
|---|
| 研究機関 | 国立情報学研究所 |
|---|
研究代表者 |
龍田 真 国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
|
|---|
| 連携研究者 |
中澤 巧爾 京都大学, 情報学研究科, 助教 (80362581)
|
|---|
| 研究期間 (年度) |
2011-04-28 – 2015-03-31
|
| 研究課題ステータス |
完了 (2014年度)
|
| 配分額 *注記 |
4,940千円 (直接経費: 3,800千円、間接経費: 1,140千円)
2014年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2013年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2012年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2011年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
|
|---|
| キーワード | 型理論 / 存在型 / 国際情報交換 / シンガポール / イタリア |
|---|
| 研究成果の概要 |
(1) 二相再帰は、関数定義の定義本体の中の全ての再帰呼び出しが同じ型をもつように制限した多相再帰である。二相再帰が主型をもち、また、決定可能な型推論をもつことを示した。(2) 双対計算を帰納型と余帰納型により拡張した。非決定可能双対計算を定義し、強正規化可能性を示した。値呼び体系と名前呼び体系を定義し、その合流性と強正規化可能性を証明した。(3) 逐次バックトラック付きゲームを提案し、そのゲーム意味論が、部分古典論理に対して、健全かつ完全な意味論を与えることを示した。
|
