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

2020 Fiscal Year Research-status Report

• Project/Area Number: 18K18030
• Research Institution: The University of Tokyo
• Principal Investigator: 佐藤 亮介 東京大学, 大学院情報理工学系研究科, 助教 (10804677)
• Project Period (FY): 2018-04-01 – 2022-03-31
• Keywords: 型システム / 値呼び評価戦略 / プログラム検証器

Outline of Annual Research Achievements

本課題では，名前呼び評価戦略を持つ関数型言語を対象とした型システムによる検証手法についての研究を進めている．本年度は，名前呼び関数型言語に対する型システムの構築を行った．まだ型システムの正しさの証明が完成していないが，これにより名前呼び関数型言語で書かれたプログラムを検証することができるようになる．また，この手法はHaskell等の必要呼び評価戦略の関数型言語にも応用することができる．さらに，本型システムは既存のHaskellのための詳細化型システムであるLiquid Haskellより真に強力，すなわち，Liquid Haskell で検証できるものは本型システムでも検証でき，Liquid Haskellで検証できないが本型システムで検証できるものがあると予想している．これについても現在証明を進めている．現在，本手法に基づく検証器のプロトタイプを作成中である．また，ここまでの研究成果をまとめ，現在，論文投稿の準備中である．
本研究課題を進める中で，名前呼び評価戦略に対する型システムだけでなく，この型システムの拡張として，名前呼び評価戦略と値呼び評価戦略を包含するようなCall-by-push-value（CBPV）評価戦略に対する型システムの設計案も得られた．これが実現できれば，評価戦略に関わらず，今までのものより広い範囲のプログラミング言語を扱える統一的な型システムとなる．この拡張後の型システムの設計，証明，および，この型システムを用いた検証器のプロトタイプの開発も今後行う．

Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

昨年度構築した名前呼び戦略に対する型システムの正しさの証明に問題が見つかり，その修正に時間を要した．

Strategy for Future Research Activity

名前呼び評価戦略を包含するCall-by-push-value（CBPV）評価戦略に対する型システムの案も得られたため，名前呼び評価戦略に限定せずに研究を行う．

Causes of Carryover

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