| 研究課題/領域番号 |
25280025
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
佐藤 雅彦 京都大学, 情報学研究科, 名誉教授 (20027387)
|
|---|
| 研究分担者 |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
桜井 貴文 千葉大学, 理学(系)研究科(研究院), 教授 (60183373)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2017-03-31
|
| キーワード | 証明支援系 / クラス理論 / 型理論 / ソフトウェアの安全性 |
|---|
| 研究実績の概要 |
ソフソフトウェアの安全性を検証するための理論として，論理学の手法を用いて形式的体系の性質の記述及び検証を数学的に厳密な方法で行なう言語体系であるロジカル・フレームワーク(論理枠組)が提案されている．形式的な計算体系であるプログラミング言語をロジカル・フレームワークで記述することにより，ソフトウェアに求められる仕様を正確に記述し，与えられたソフトウェアがその仕様を満足することを厳密に検証することが可能になる．さらにロジカル・フレームワークを計算機上に実装することができれば，これらの記述・検証の機械的に正確な検査が可能となり，ソフトウェアの品質面，安全面の信頼性が高まることが期待される．
変数の束縛機構は，プログラミング言語とくに関数型言語における基本的な研究課題であり多数の研究者により長年研究がされてきている．今年度の研究では，自由変数を含まない閉じたλ項の全体を帰納的に定義するという問題を解決することができた．この定義の方法を実装することにより，様々なメタ定理の証明が簡潔に行なえるようになることが期待できる．
またロジカル・フレームワークの基礎となるクラス理論の実装について考察を行った．その結果，クラス理論はフレーゲが『算術の基本法則』で導入した値域の概念と密接に関係することがわかった．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
変数の束縛機構に関して，自由変数を一切用いることなく，閉じたλ項を定義する方法を確立できたことは大きな収穫であった．
また，クラス理論とフレーゲの値域の概念との関連についての研究も開始することができた．
以上のことにより，研究は順調に進展していると考える．
|
| 今後の研究の推進方策 |
自由変数を用いないで閉じたλ項を定義する方法をクラス理論に導入する．これにより，メタ定理の証明がどのように簡略化できるかについて考察し，クラスのインスタンスの実現方法を検討する予定である．
ロジカル・フレームワーク実装のためのプログラミング言語の設計の詳細化を行ない予備的な実装を行なう．
|
| 次年度使用額が生じた理由 |
白内障手術のため26年度中に2回入院した。そのため計画していた出張を複数回中止した。
|
| 次年度使用額の使用計画 |
26年度に中止した出張のための費用に充てる。
|
