2015 Fiscal Year Annual Research Report
高階・型付きの計算体系に基づくプログラミングの理論と応用の展開
| Project/Area Number |
15H02681
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
住井 英二郎 東北大学, 情報科学研究科, 教授 (00333550)
|
|---|
| Project Period (FY) |
2015-04-01 – 2020-03-31
|
| Keywords | ソフトウェア基礎 / 関数型言語 / 型システム / セキュリティ / プログラム検証 |
|---|
| Outline of Annual Research Achievements |
本研究の目的は次のとおりである。古くから研究されているが最近になって目覚ましく実用化が進み産業界でも注目されている「関数型言語」を中心とする、高階・型付き計算およびプログラミングの理論の深化と応用の拡大を目指す。具体的には (1) 標準的な型システムを利用した、軽量で実用的な静的プログラム検証 (2) プログラミング以外へのプログラミング言語理論の展開 の2つを中心的テーマとする。前者の例としては研究代表者らが研究・開発中の実用的な静的サイズ検査つき線形演算ライブラリの設計と実装、後者の例としてはパラメタ的高階抽象構文に基づく構造化グラフ表現の理論の構築や、OAuth, OpenIDといった現実的認可プロトコルの型システムに基づく検証を行う。
本年度の研究実施計画は以下のとおりであった。研究目的の項で述べた「(1) 標準的な型システムを利用した、軽量で実用的な静的プログラム検証」のfirst instanceとして、研究協力者の大学院生（平成27年度時点で博士前期課程2年）と平成25年度から研究・開発中の実用的な静的サイズ検査つき線形演算ライブラリ「SLAP」の設計と実装を完成する。SLAPは、FortranやCなどのプログラミング言語で広く用いられている標準的な線形演算ライブラリであるBLASおよびLAPACKのOCamlバインディングであるLACAMLに、静的サイズ検査のための型をつけたインターフェースである。
本年度は以上の目的と計画にもとづいて研究を実施し、その成果を雑誌論文"A Simple and Practical Linear Algebra Library Interface with Static Size Checking", EPTCS 198, pp. 1-21（研究協力者と研究代表者の共著）他として発表した。
|
| 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 |
構造化グラフ表現の構築や、認可プロトコルの検証を例とする、高階・型付き計算およびプログラミングの理論の深化と応用の拡大を引き続き目指す。
|
Research Products
(7 results)
