| 研究課題/領域番号 |
25330096
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 鶴見大学 (2015)
国立情報学研究所 (2013-2014) |
|---|
研究代表者 |
田辺 良則 鶴見大学, 文学部, 教授 (60443199)
|
|---|
| 研究分担者 |
萩谷 昌己 東京大学, 大学院情報理工学系研究科, 教授 (30156252)
山本 光晴 千葉大学, 大学院理学研究科, 准教授 (00291295)
|
|---|
| 研究協力者 |
湯浅 能史
逸見 港
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| 研究課題ステータス |
完了 (2015年度)
|
| 配分額 *注記 |
4,680千円 (直接経費: 3,600千円、間接経費: 1,080千円)
2015年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
2014年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
2013年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
|
|---|
| キーワード | 定理証明支援系 / ソフトウェア検証 / ディペンダブル・コンピューティング / Coq / 型推論 / コード抽出 |
|---|
| 研究成果の概要 |
定理証明支援系Coqから，プログラミング言語Scalaへのコード抽出を実現した．Coqによって，コードが正しく動作することの証明を記述した上でコード抽出をすれば，抽出されたコードの正しさが保証される．Scalaコードは，Javaで記述された多数のシステムと親和性が高いと期待される．コード抽出を行うコード自体もCoqで記述されており，その動作が妥当であることが，Coq上の証明として与えられている．
|
