2013 Fiscal Year Research-status Report
依存型理論による安全性保証付きデータ構造の創出・推論・進化
| Project/Area Number |
24300001
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
浜名 誠 群馬大学, 理工学研究科, 助教 (90334135)
|
|---|
| Project Period (FY) |
2012-04-01 – 2015-03-31
|
| Keywords | プログラム理論 / 代数理論 / 依存型 / データ構造 / 情報学基礎 / プログラム意味論 / 多相型 |
|---|
| Research Abstract |
本年度は、依存型を形式的に論じるためのモデルの等式論理の確立を行った。結果、様々な多相システムを統一的に扱うための体系である多相型代数理論を構築することに成功した。一般化依存多項式を用いることで、任意のシグネチャによる多相型構文と項中の型の代入を厳密にモデル化することができた。そして代数的モデルを持つ論理体系を圏論的考察から導出し、その正当性を証明した。特に多相型の型宇宙はΣモノイドであることを明らかにし、これにより複数の型宇宙の間の変換を議論することが可能となった。これにより既存の種々の型理論とモデルを統一、単純化し、その本質を明確化する理論となった。また、この体系が確かに様々な実際例を統一的に扱うことができることを実際に例示することにより示した。これをまとめた論文は、理論計算機科学のトップ国際会議 ACM/IEEE Logic in Computer Science (LICS'13)に採択され、IEEE Pressから出版された。
|
| 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 |
本年度は、The European Joint Conferences on Theory and Practice of Software (ETAPS)併設の国際ワークショップMathematically Structured Functional Programming 2014のプログラム委員、および国内最大のプログラミング言語会議PPLのプログラム委員を務め、型理論および関数型プログラミングの最新進展状況を把握し、関連研究者から有用な研究推進の情報を得た。今後はこれらも参考にし、依存型の計算機構の研究を進める。
|
| Expenditure Plans for the Next FY Research Funding |
前倒し申請をした分が、その後の研究の進行が当初どおりだったため実際は使用しなかった。
当初の予定通りに使用する。
|
