| 研究課題/領域番号 |
25280025
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 一部基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
佐藤 雅彦 京都大学, 情報学研究科, 名誉教授 (20027387)
|
|---|
| 研究分担者 |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
桜井 貴文 千葉大学, 理学(系)研究科(研究院), 教授 (60183373)
|
|---|
| 連携研究者 |
小林 直樹 東京大学, 情報理工学系研究科, 教授 (00262155)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2017-03-31
|
| 研究課題ステータス |
完了 (2016年度)
|
| 配分額 *注記 |
17,550千円 (直接経費: 13,500千円、間接経費: 4,050千円)
2016年度: 3,250千円 (直接経費: 2,500千円、間接経費: 750千円)
2015年度: 4,030千円 (直接経費: 3,100千円、間接経費: 930千円)
2014年度: 4,680千円 (直接経費: 3,600千円、間接経費: 1,080千円)
2013年度: 5,590千円 (直接経費: 4,300千円、間接経費: 1,290千円)
|
|---|
| キーワード | クラス理論 / 型理論 / 証明検証 / ソフトウェアの安全性 / 仕様記述・検証 / 証明支援系 |
|---|
| 研究成果の概要 |
ソフトウェアの安全性を検証するための理論として，論理学の手法を用いて形式的体系の性質の記述及び検証を数学的に厳密な方法で行う言語体系である論理枠組が提案されている本研究では，従来の論理枠組は型理論の上に構築されているのに対してクラス理論の上に構築することを実現した．
ここでのクラス理論は本研究で新しく提案した理論であり，型理論にない柔軟性があり，さらにクラス全体のクラスを矛盾なく扱えるという特徴がある．この特徴のため，論理枠組の中で，枠組自身に言及し，その構造を解析することができた．とくに重要な成果として，変数の束縛機構を分析し，α同値性の概念について新しい見方での定義を与えることができた．
|
