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