Deepening of a self-extendable software verification system based on class theory

2022 Fiscal Year Final Research Report

• Project/Area Number: 17H01724
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: Kyoto University
• Principal Investigator: Sato Masahiko 京都大学, 情報学研究科, 名誉教授 (20027387)
• Co-Investigator(Kenkyū-buntansha): 桜井 貴文 千葉大学, 大学院理学研究院, 教授 (60183373) ; 亀山 幸義 筑波大学, システム情報系, 教授 (10195000) ; 五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
• Project Period (FY): 2017-04-01 – 2021-03-31
• Keywords: クラス理論 / 型理論 / 証明検証 / ソフトウェアの安全性

Outline of Final Research Achievements

In order to verify the safety of software, the concept of Logical Framework is proposed. A logical framework can be used to internally realize formal systems and prove their properties in a rigorous manner. In contrast to the fact that most logical frameworks are based on type theory, we realized our logical framework based on class theory.
We proposed the new class theory in this research. The class theory is more flexible than type theories and enjoys the property that it can deal with the class of all classes in a consistent way. Due to this property, our logical framework can refer to the framework itself and can analyze its structure by itself. We analyzed the mechanism of variable binding in the lambda calculus, and could show the equivalence of lambda-calculus and combinatory logic.

Free Research Field

ソフトウェアの基礎理論

Academic Significance and Societal Importance of the Research Achievements

社会基盤としての計算機の重要性の増加により,ソフトウェアの安全性など,ソフトウェの品質に対する要求はますます高まっている.
本研究は,バグのないソフトウェアを構築するためのクラス理論に基づく理論的基盤を与え,さらにそれを用いて(ユーザによる自己拡張を許す)自然枠組(Natural Framework)とよばれるソフトウェア実行および検証環境を提供するものであり，大いに学術的意義，社会的意義がある．