Program verification by refinment type system for call-by-name programs
| 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
|
| Project Status |
Completed (Fiscal Year 2022)
|
| Budget Amount *help |
¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000)
Fiscal Year 2021: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2020: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2019: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2018: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
|
|---|
| 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.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究は近年注目されるようになってきた関数型言語、特にHaskellやCleanなどの名前呼び評価戦略の言語に対する全自動検証の第一歩である。本研究では、そのような言語の核となる小さな言語に対する全自動検証手法を提案し、実装、実験を行うことができた。本研究を発展させることによってHaskell等のプログラムを全自動で検証することができる可能性がある。既存研究としてHaskellを検証するための手法はあるが、全自動ではないという点が本研究手法との大きな違いである。
|
Report
(6 results)
Research Products
(1 results)
