| 研究課題/領域番号 |
22300008
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウエア
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
佐藤 雅彦 京都大学, 大学院・情報学研究科, 名誉教授 (20027387)
|
|---|
| 研究分担者 |
湯淺 太一 (湯浅 太一) 京都大学, 大学院・情報学研究科, 名誉教授 (60158326)
山本 章博 京都大学, 大学院・情報学研究科, 教授 (30230535)
五十嵐 淳 京都大学, 大学院・情報学研究科, 教授 (40323456)
中澤 巧爾 京都大学, 大学院・情報学研究科, 助教 (80362581)
|
|---|
| 研究期間 (年度) |
2010 – 2012
|
| 研究課題ステータス |
完了 (2012年度)
|
| 配分額 *注記 |
17,940千円 (直接経費: 13,800千円、間接経費: 4,140千円)
2012年度: 4,420千円 (直接経費: 3,400千円、間接経費: 1,020千円)
2011年度: 6,110千円 (直接経費: 4,700千円、間接経費: 1,410千円)
2010年度: 7,410千円 (直接経費: 5,700千円、間接経費: 1,710千円)
|
|---|
| キーワード | ソフトウェア検証 / クラス理論 / ソフトウェアの安全性 / 型理論 / 項書換 / 自然枠組 / ソフトウェア開発 / メタ言語 / メタ理論 / 式の理論 / 抽象操作 |
|---|
| 研究概要 |
本研究では,ソフトウェアの安全性を保障するための方法論として, バグのないソフトウェアを構築する環境を実現することの重要性を指摘し, 具体的なシステムのプロトタイプを実装した. とくに, 計算と論理を融合した, 新しいプログラミング言語を設計・実装し, その言語を用いてシステムを実装した. このため, 実装したシステム自体の安全性についても, 原理的に検証可能である. システムとユーザとのインターフェースもこの言語を用いて実装した
|
