Program verification by refinment type system for call-by-name programs

2022 Fiscal Year Final Research Report

• Project/Area Number: 18K18030
• Research Category: Grant-in-Aid for Early-Career Scientists
• Allocation Type: Multi-year Fund
• Review Section: Basic Section 60050:Software-related
• Research Institution: The University of Tokyo (2020-2022); Kyushu University (2018-2019)
• Principal Investigator: Sato Ryosuke 東京大学, 大学院情報理工学系研究科, 助教 (10804677)
• Project Period (FY): 2018-04-01 – 2023-03-31
• Keywords: 型システム / 名前呼び評価戦略 / 関数型言語 / 全自動検証

Outline of Final Research Achievements

Based on the research plan, we were able to progress with the study and develop a verifier for a call-by-name functional language. Specifically, we managed the evaluation timing of terms bound to variables using a substructural type system, and by determining whether the information of the term can be used based on its evaluation timing, we were able to construct a sound refinement type system for the call-by-value language. Furthermore, we introduced the concept of type guards, which was not necessary in a type system of call-by-value language, allowing us to build a type system with sufficient expressive power. To verify the effectiveness of this approach, we implemented a verifier and conducted evaluations.

Free Research Field

形式検証

Academic Significance and Societal Importance of the Research Achievements

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