| 研究課題/領域番号 |
17H01724
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
佐藤 雅彦 京都大学, 情報学研究科, 名誉教授 (20027387)
|
|---|
| 研究分担者 |
桜井 貴文 千葉大学, 大学院理学研究院, 教授 (60183373)
亀山 幸義 筑波大学, システム情報系, 教授 (10195000)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2021-03-31
|
| 研究課題ステータス |
完了 (2022年度)
|
| 配分額 *注記 |
18,200千円 (直接経費: 14,000千円、間接経費: 4,200千円)
2020年度: 4,030千円 (直接経費: 3,100千円、間接経費: 930千円)
2019年度: 4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2018年度: 4,680千円 (直接経費: 3,600千円、間接経費: 1,080千円)
2017年度: 5,200千円 (直接経費: 4,000千円、間接経費: 1,200千円)
|
|---|
| キーワード | クラス理論 / 型理論 / 証明検証 / ソフトウェアの安全性 / 仕様記述・検証 / 証明支援系 |
|---|
| 研究成果の概要 |
ソフトウェアの安全性を検証するための理論として,論理学の手法を用いて形式的体系の性質の記述及び検証を数学的に厳密な方法で行う言語体系である論理枠組が提案されている.本研究では,従来の論理枠組は型理論の上に構築されているのに対してクラス理論の上に構築することを実現した.
ここでのクラス理論は本研究で新しく提案した理論であり,型理論にない柔軟性があり,さらにクラス全体のクラスを矛盾なく扱えるという特徴がある.この特徴のため,論理枠組の中で,枠組自身に言及し,その構造を解析することができた.とくに重要な成果として,変数の束縛機構を分析し,λ計算とコンビネータ論理の同値性を示すことができた．
|
| 研究成果の学術的意義や社会的意義 |
社会基盤としての計算機の重要性の増加により,ソフトウェアの安全性など,ソフトウェの品質に対する要求はますます高まっている.
本研究は,バグのないソフトウェアを構築するためのクラス理論に基づく理論的基盤を与え,さらにそれを用いて(ユーザによる自己拡張を許す)自然枠組(Natural Framework)とよばれるソフトウェア実行および検証環境を提供するものであり，大いに学術的意義，社会的意義がある．
|
