| 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
|
| Project Status |
Completed (Fiscal Year 2022)
|
| Budget Amount *help |
¥18,200,000 (Direct Cost: ¥14,000,000、Indirect Cost: ¥4,200,000)
Fiscal Year 2020: ¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000)
Fiscal Year 2019: ¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2018: ¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2017: ¥5,200,000 (Direct Cost: ¥4,000,000、Indirect Cost: ¥1,200,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 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.
|
| Academic Significance and Societal Importance of the Research Achievements |
社会基盤としての計算機の重要性の増加により,ソフトウェアの安全性など,ソフトウェの品質に対する要求はますます高まっている.
本研究は,バグのないソフトウェアを構築するためのクラス理論に基づく理論的基盤を与え,さらにそれを用いて(ユーザによる自己拡張を許す)自然枠組(Natural Framework)とよばれるソフトウェア実行および検証環境を提供するものであり，大いに学術的意義，社会的意義がある．
|
