| 研究成果の概要 |
ソフトウェアの安全性を検証するための理論として,論理学の手法を用いて形式的体系の性質の記述及び検証を数学的に厳密な方法で行う言語体系である論理枠組が提案されている.本研究では,従来の論理枠組は型理論の上に構築されているのに対してクラス理論の上に構築することを実現した.
ここでのクラス理論は本研究で新しく提案した理論であり,型理論にない柔軟性があり,さらにクラス全体のクラスを矛盾なく扱えるという特徴がある.この特徴のため,論理枠組の中で,枠組自身に言及し,その構造を解析することができた.とくに重要な成果として,変数の束縛機構を分析し,λ計算とコンビネータ論理の同値性を示すことができた．
|
| 研究成果の学術的意義や社会的意義 |
社会基盤としての計算機の重要性の増加により,ソフトウェアの安全性など,ソフトウェの品質に対する要求はますます高まっている.
本研究は,バグのないソフトウェアを構築するためのクラス理論に基づく理論的基盤を与え,さらにそれを用いて(ユーザによる自己拡張を許す)自然枠組(Natural Framework)とよばれるソフトウェア実行および検証環境を提供するものであり，大いに学術的意義，社会的意義がある．
|
