| 研究課題/領域番号 |
18500005
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎
|
|---|
| 研究機関 | お茶の水女子大学 |
|---|
研究代表者 |
浅井 健一 お茶の水女子大学, 大学院・人間文化創成科学研究科, 准教授 (10262156)
|
|---|
| 連携研究者 |
亀山 幸義 筑波大学, 大学院・システム情報工学研究科, 准教授 (10195000)
|
|---|
| 研究期間 (年度) |
2006 – 2009
|
| 研究課題ステータス |
完了 (2009年度)
|
| 配分額 *注記 |
3,890千円 (直接経費: 3,200千円、間接経費: 690千円)
2009年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2008年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2007年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2006年度: 900千円 (直接経費: 900千円)
|
|---|
| キーワード | プログラム理論 / 部分継続 / 情報基礎 |
|---|
| 研究概要 |
従来の単相の型システムを拡張して多相の型システムを提案し、その健全性など各種の性質を証明した。また、健全性は定理証明系Coqを用いて定式化した。限定継続命令の定義を与えるインタプリタを系統的に変換することでスタックの複製などを行う低レベレな処理系を導けることを示した。それに基づいて、実際に機械語を出力するコンパイラを作成した。また、限定継続命令の応用とそてprintfの型付けが限定継続を用いると極めて自然に書けることを示した。
|
