Construction of a self-extendable software verification system based on class theory
| 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
|
| Project Status |
Completed (Fiscal Year 2016)
|
| Budget Amount *help |
¥17,550,000 (Direct Cost: ¥13,500,000、Indirect Cost: ¥4,050,000)
Fiscal Year 2016: ¥3,250,000 (Direct Cost: ¥2,500,000、Indirect Cost: ¥750,000)
Fiscal Year 2015: ¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000)
Fiscal Year 2014: ¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2013: ¥5,590,000 (Direct Cost: ¥4,300,000、Indirect Cost: ¥1,290,000)
|
|---|
| 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.
|
Report
(5 results)
Research Products
(21 results)
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
[Presentation] 私の基礎研究2015
Author(s)
佐藤雅彦
Organizer
日本ソフトウェア科学会第32回大会
Place of Presentation
早稲田大学理工学部
Year and Date
2015-09-10
Related Report
Invited
-
[Presentation] 計算と論理2015
Author(s)
佐藤 雅彦
Organizer
情報処理学会 第77回全国大会
Place of Presentation
京都大学
Year and Date
2015-03-17
Related Report
Invited
-
[Presentation] A name-free lambda calculus2015
Author(s)
Masahiko Sato
Organizer
JAIST Logic Workshop Series 2015: Constructivism and Computablility
Place of Presentation
Shiinoki Cultural Complex, Kanazawa
Year and Date
2015-03-02 – 2015-03-06
Related Report
Invited
-
-
