| 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)
|
|---|
| 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.
|
