名前呼び計算体型のための型システムによるプログラム検証

2018 Fiscal Year Research-status Report

• Project/Area Number: 18K18030
• Research Institution: Kyushu University
• Principal Investigator: 佐藤 亮介 九州大学, システム情報科学研究院, 助教 (10804677)
• Project Period (FY): 2018-04-01 – 2022-03-31
• Keywords: 型システム / 名前呼び評価戦略 / 高階関数型言語 / プログラム検証

Outline of Annual Research Achievements

本課題では，名前呼び評価戦略を持つ関数型言語を対象とした型システムによる検証手法についての研究を進めている．本年度は，名前呼び関数型言語の核となる単純な言語（単純型付きラムダ計算の簡単な拡張）に対して型システムを構築し，その健全性を証明した．これにより，名前呼び関数型言語で書かれたプログラムを検証することができるようになった．また，この手法はHaskell等の必要呼び評価戦略の関数型言語にも応用することができる．現在，本手法に基づく検証器のプロトタイプを作成中である．また，ここまでの研究成果をまとめ，現在，論文投稿の準備中である．
型システムを構築する際，当初は認識できていなかった課題がいくつか見つかった．主に，型システムの精度が悪い（検証できてほしいプログラムが検証できない）という問題があったが，解決策を見つけている．具体的には，値呼びのプログラムでは関数を呼び出す際に引数部分が評価されるため，評価が失敗しないための事前条件は関数の呼び出し時点で検証すればよい．しかし，名前呼びのプログラムでは，関数を呼び出しただけでは引数部分は評価されず，実際にその引数が使われる時点で検証しなければならない．これを実現するためには既存の値呼び用の型システムからの本質的な改良が必要となった．この問題を解決するため引数の事前条件を表現できるように型を拡張した．また，Liquid Haskellの型システムと我々の型システムが比較不能であることを明らかにした．これについては，Liquid Haskellの手法の一部を用いることで，どちらの型システムよりも高精度な型システムを構築することができると考えている．

Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

名前呼び戦略を持つ関数型言語に対する十分な検証能力を持つ型システムが構築できた．新たな課題が出てきたため，申請書の計画とは異なっているが，有用な結果が得られている．

Strategy for Future Research Activity

引き続き計画に従って研究を進める．
理論的な成果が出ている一方，実験が計画より遅れているため，実装・実験に注力する．

Causes of Carryover

英語論文についての校正費は，今年度中に投稿準備が完了しなかったため計上しなかった．これを来年度の英文校正費に当てる．