| 研究実績の概要 |
本研究の目的は次のとおりである。古くから研究されているが最近になって目覚ましく実用化が進み産業界でも注目されている「関数型言語」を中心とする、高階・型付き計算およびプログラミングの理論の深化と応用の拡大を目指す。具体的には (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（研究協力者と研究代表者の共著）他として発表した。
|
