2022 Fiscal Year Annual Research Report
Program verification by refinment type system for call-by-name programs
| Project/Area Number |
18K18030
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
佐藤 亮介 東京大学, 大学院情報理工学系研究科, 助教 (10804677)
|
|---|
| Project Period (FY) |
2018-04-01 – 2023-03-31
|
| Keywords | 関数型言語 / 名前呼び評価戦略 / 型システム / 全自動検証 |
|---|
| Outline of Annual Research Achievements |
ソフトウェアが社会の至る所で用いられるようになり、その安全性が非常に重要になっている。ソフトウェアの安全性を形式的に保証するため様々な手法が提案されており、それらの手法に基づいた検証器も積極的に開発、使用されている。しかしながら、近年注目されるようになってきた関数型言語に対しては、検証に関する研究が進んでおらず、特に、名前呼び戦略の言語に対する自動検証の研究はほとんど行われていない。今後さらに多くの開発者が名前呼び戦略の言語を使用していくものと考えられるため、これらの言語に対する検証手法の開発が強く望まれる。そこで本課題では，名前呼び評価戦略を持つ関数型言語を対象とした型システムによる検証手法についての研究を進めた．名前呼び関数型言語に対する型システムの構築を行い，型推論の手法を提案した．またこれらの手法を基にした名前呼びプログラムの全自動検証器を実装した．これにより名前呼び関数型言語で書かれた小さなプログラムの安全性を全自動検証することができるようになった．また，この手法はHaskell等の必要呼び評価戦略の関数型言語に応用することができると考え，本研究を発展させることによりHaskellプログラム等の現実的なプログラムの全自動検証が実現できると考えている．
本研究課題を進める中で，名前呼び評価戦略に対する型システムだけでなく，この型システムの拡張として，名前呼び評価戦略と値呼び評価戦略を包含するようなCall-by-push-value（CBPV）評価戦略に対する型システムの設計案も得られた．これが実現できれば，評価戦略に関わらず，今までのものより広い範囲のプログラミング言語を扱える統一的な型システムとなる．
|
Research Products
(1 results)
