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

2016 Fiscal Year Final Research Report

• Project/Area Number: 25280025
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Partial Multi-year Fund
• Section: 一般
• Research Field: Software
• Research Institution: Kyoto University
• Principal Investigator: Sato Masahiko 京都大学, 情報学研究科, 名誉教授 (20027387)
• Co-Investigator(Kenkyū-buntansha): 外山 芳人 東北大学, 電気通信研究所, 教授 (00251968) ; 五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456) ; 桜井 貴文 千葉大学, 理学(系)研究科(研究院), 教授 (60183373)
• Co-Investigator(Renkei-kenkyūsha): KOBAYASHI Naoki 東京大学, 情報理工学系研究科, 教授 (00262155)
• Project Period (FY): 2013-04-01 – 2017-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 classed 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 give a new definition of the notion of the alpha-equivalence.

Free Research Field

ソフトウェアの基礎理論