| 研究課題/領域番号 |
24500012
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎
|
|---|
| 研究機関 | 岐阜大学 (2013-2016)
名古屋大学 (2012) |
|---|
研究代表者 |
草刈 圭一朗 岐阜大学, 工学部, 教授 (90323112)
|
|---|
| 研究分担者 |
坂部 俊樹 名古屋大学, 情報科学研究科, 教授 (60111829)
|
|---|
| 連携研究者 |
酒井 正彦 名古屋大学, 情報科学研究科, 教授 (50215597)
西田 直樹 名古屋大学, 情報科学研究科, 准教授 (00397449)
|
|---|
| 研究期間 (年度) |
2012-04-01 – 2017-03-31
|
| 研究課題ステータス |
完了 (2016年度)
|
| 配分額 *注記 |
5,070千円 (直接経費: 3,900千円、間接経費: 1,170千円)
2016年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2015年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2014年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2013年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2012年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
|
|---|
| キーワード | 関数型プログラム / 停止性 / 再帰定義 / 情報基礎 / 関数プログラム |
|---|
| 研究成果の概要 |
我々はSML系の関数型言語そのものと呼んでもよい構文を持つ書換えモデルを定式化した．理論的には，高階関数，多相型，代数的データ型，パターンを用いた関数抽象の４つの拡張を行っている．このモデル上に，パターンを用いた関数抽象への対応が不十分ではあるものの，静的な再帰構造解析に基づく停止性証明法である静的依存対法と，その補助理論となる簡約化順序，引数切り落とし法，実効規則の3つの理論構築を行い，得られた理論成果とSMTソルバとの連携に基づいた関数型プログラム停止性証明ツールの作成を行った．これらの拡張により実用性が劇的に向上し，実在のプログラム検証へ多大な貢献が期待できることになる．
|
