| 研究課題/領域番号 |
25280020
|
|---|
| 研究機関 | 筑波大学 |
|---|
研究代表者 |
亀山 幸義 筑波大学, システム情報系, 教授 (10195000)
|
|---|
| 研究分担者 |
浅井 健一 お茶の水女子大学, 基幹研究院, 准教授 (10262156)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
海野 広志 筑波大学, システム情報系, 助教 (80569575)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | ディペンダブルコンピューティング / 関数型プログラミング言語 / 実行時プログラム生成 / プログラム検証 / プログラム変換 / プログラム特化 / 高性能計算 |
|---|
| 研究実績の概要 |
本研究の最終年度にあたり、これまでの研究成果のまとめとなる研究および論文執筆・論文発表等をおこなった。
（１） 高性能計算のためのコード生成法の研究では、CPUのベクトル命令や融合演算などを関数型言語OCamlから直接操作するためのDSLを設計し、終タグレス法を用いてモジュラーに表現されたコード生成器で、行列乗算や高速フーリエ変換などの高性能コードを生成できることを実証した[FHCP2015]。
（２）前年度の成果である拡張可能な統合言語クエリと、モジュールのコード生成に関する論文を執筆し国際会議で発表した[PEPM2016]
（３）自動でコード生成を行う部分評価と手動でコード生成部分を指示する段階的計算の間の関係を明らかにした [PEPM2016]。さらに、ふたつの手法の関係を精査することで、段階的計算では明らかではなかった「最もよい注釈」を定義し、部分評価の束縛時解析を通して得られる注釈が最も良いものであることを示した [SCSS2016]。
（４）コード生成器が必ず安全なコードを生成することを保証するための型システムの研究を行った．特に cross-stage persistence (CSP) と呼ばれる，コード内にコード生成時に計算した結果を埋めこむための機構について、MLの値多相・参照機構と素朴に組み合わせると安全性が損なわれることが知られている．この問題を解決するための新しい型システムを提案した[JSSST2015]。
（５）高レベルプログラムの検証のための形式体系であるリファインメント型システム上の型推論問題を、多目的最適化問題として一般化したリファインメント型最適化問題を提案し、実際にそのような最適化問題を解くための、制約最適化に基づく新手法を開発した[SAS2015]。
|
| 現在までの達成度 (段落) |
27年度が最終年度であるため、記入しない。
|
| 今後の研究の推進方策 |
27年度が最終年度であるため、記入しない。
|
| 次年度使用額が生じた理由 |
27年度が最終年度であるため、記入しない。
|
| 次年度使用額の使用計画 |
27年度が最終年度であるため、記入しない。
|
