| 研究課題/領域番号 |
15K12007
|
|---|
| 研究種目 |
挑戦的萌芽研究
|
| 配分区分 | 基金 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 筑波大学 |
|---|
研究代表者 |
亀山 幸義 筑波大学, システム情報系, 教授 (10195000)
|
|---|
| 研究協力者 |
坂口 和彦 筑波大学, システム情報工学研究科
渡部 恭久 筑波大学, システム情報工学研究科
大石 純平 筑波大学, システム情報工学研究科
薄井 千春 筑波大学, システム情報工学研究科
須藤 悠斗 筑波大学, システム情報工学研究科
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| 研究課題ステータス |
完了 (2017年度)
|
| 配分額 *注記 |
3,510千円 (直接経費: 2,700千円、間接経費: 810千円)
2017年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2016年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2015年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
|
|---|
| キーワード | 証明記述言語 / プログラム生成 / メタプログラミング / コントロールエフェクト / 副作用 / 型安全性 / モジュール / 定理証明支援システム / プログラム抽出・生成 / 型システム / スコープ安全性 / 定理証明系 / 形式検証 / 証明の自動化 / プログラム抽出 / 証明探索 / 証明の生成 |
|---|
| 研究成果の概要 |
本研究はメタプログラミングの手法・研究成果を、定理証明系における証明記述言語に適用することを目的とした研究である。メタプログラミングの中でも静的な型付けによる安全性の保証を与える手法に基づいて、破壊的変数や限定継続などのコントロールオペレータを用いてコード生成器の記述言語の表現力を高めるとともに、生成されるコードの記述言語にモジュールを追加した場合の拡張についても考察し、いずれも健全性が成立し一定の記述力をもつ型システムの設計に成功した。これを用いて非常に簡単な証明記述言語を設計し、副作用を含む証明生成器を記述する手法にについての知見を得ることができた。
|
