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

2019 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

3: Progress in research has been slightly delayed.

Reason

名前呼び戦略を持つ関数型言語に対する型システムを構築してきたが，検証能力に若干の問題が含まれていることがわかり，その修正に時間を要した．

Strategy for Future Research Activity

引き続き計画に従って研究を進める.

Causes of Carryover

英語論文についての校正費は，今年度中に投稿準備が完了しなかったため計上しなかった．これを次年度の英文校正費に当てる．
また，新型コロナウィルスの影響で出張ができなかったため，旅費を計上しなかった．こちらも次年度の旅費に当てる．