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

2022 年度 研究成果報告書

• 研究課題/領域番号: 18K18030
• 研究種目: 若手研究
• 配分区分: 基金
• 審査区分: 小区分60050:ソフトウェア関連
• 研究機関: 東京大学 (2020-2022); 九州大学 (2018-2019)
• 研究代表者: 佐藤 亮介 東京大学, 大学院情報理工学系研究科, 助教 (10804677)
• 研究期間 (年度): 2018-04-01 – 2023-03-31
• キーワード: 型システム / 名前呼び評価戦略 / 関数型言語 / 全自動検証

研究成果の概要

研究計画に基づき研究を進め、名前呼び戦略の言語のための検証手法を構築することができた。具体的には、変数に束縛される項がいつ評価されるのかを部分構造型システムを用いることによって管理し、評価されるタイミングによってその項の情報を使えるかどうかを判断することによって名前呼び評価戦略の言語のための健全な詳細化型システムを構築することができた。さらに、値呼び評価戦略の言語のための型システムでは必要ではなかった型ガードという概念を導入することによって十分な表現力を持った型システムを構築することができた。本手法の効果を確かめるため検証器を実装し、評価を行った。

自由記述の分野

形式検証

研究成果の学術的意義や社会的意義

本研究は近年注目されるようになってきた関数型言語、特にHaskellやCleanなどの名前呼び評価戦略の言語に対する全自動検証の第一歩である。本研究では、そのような言語の核となる小さな言語に対する全自動検証手法を提案し、実装、実験を行うことができた。本研究を発展させることによってHaskell等のプログラムを全自動で検証することができる可能性がある。既存研究としてHaskellを検証するための手法はあるが、全自動ではないという点が本研究手法との大きな違いである。