2012 Fiscal Year Research-status Report
依存型理論による安全性保証付きデータ構造の創出・推論・進化
| Project/Area Number |
24300001
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Research Institution | Gunma University |
|---|
Principal Investigator |
浜名 誠 群馬大学, 大学院・工学研究科, 助教 (90334135)
|
|---|
| Project Period (FY) |
2012-04-01 – 2015-03-31
|
| Keywords | 関数プログラム / 依存型 / 情報学基礎 / 自動定理証明 / データ構造 |
|---|
| Research Abstract |
本年度は、データ構造中のループ要素を特徴付ける研究を行った。Haskell言語は再帰的定義により循環データ構造を定義することができる。さらに、言語要素アローを用いるとループを含む計算の新しいプログラミングができる。循環データ構造とループの計算というこれら一見異なるプログラム要素には実際は共通の原理があることを明らかにした。これはトレース付きフレイド圏を用いるもので、圏論的解釈を異なる実例に対して用いると、循環データ構造やループのある計算の様々なパターンを統一的に導出できることが分かった。この結果は国際会議11th International Symposium on Functional and Logic Programmingで発表し、Springer-Verlagから出版された。
また第16回群馬大学横山科学技術賞を「依存型による安全で高信頼なソフトウェアの基礎研究」にて受賞した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
安全なデータ構造の依存型としての表現方法としてアロー付きループ要素とその圏論的構造という特徴的なケースを明らかにできた。
|
| Strategy for Future Research Activity |
本年度は、名古屋大学で開催されたRTAの一つとして開催された国際ワークショップ6th International Workshop on Higher-Order Rewritingの議長をつとめ、依存型プログラミングにも重要な高階計算研究の最新進展状況を把握し、依存型と型無し計算の間の関係について関連研究者から有用な研究推進の情報を得た。今後はこれらも参考にし、依存型の推論と計算機構への研究へ進める。
木構造の依存型のためには、木の大小関係を表す多相性が必要であることを認識した。このために、一般的な多相型のための等式推論体系を構築することも今後の研究の促進に必要であることを認識した。
|
| Expenditure Plans for the Next FY Research Funding |
次年度以降も国内、外国とも旅費を主に用いる。これは、
(1)本研究の中心となる依存型システムの最新の研究成果に追従し本研究に反映させるため(調査・研究旅費)
(2)理論と実装の構築には特に海外の関連研究者との議論を重ねることが研究を進める上での重要な促進方法であるため(研究打合せ旅費)
(3)申請者の研究結果を衆知させるためにである(成果発表)。
また設備備品として、研究内容の依存型プログラミングによるデータ構造の実装と解析にサーバ型PCを導入する予定である。
|
Research Products
(5 results)
