2014 Fiscal Year Annual Research Report
クラス理論に基づく自己拡張可能なソフトウェア検証体系の構築
| Project/Area Number |
25280025
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
佐藤 雅彦 京都大学, 情報学研究科, 名誉教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
桜井 貴文 千葉大学, 理学(系)研究科(研究院), 教授 (60183373)
|
|---|
| Project Period (FY) |
2013-04-01 – 2017-03-31
|
| Keywords | 証明支援系 / クラス理論 / 型理論 / ソフトウェアの安全性 |
|---|
| Outline of Annual Research Achievements |
ソフソフトウェアの安全性を検証するための理論として，論理学の手法を用いて形式的体系の性質の記述及び検証を数学的に厳密な方法で行なう言語体系であるロジカル・フレームワーク(論理枠組)が提案されている．形式的な計算体系であるプログラミング言語をロジカル・フレームワークで記述することにより，ソフトウェアに求められる仕様を正確に記述し，与えられたソフトウェアがその仕様を満足することを厳密に検証することが可能になる．さらにロジカル・フレームワークを計算機上に実装することができれば，これらの記述・検証の機械的に正確な検査が可能となり，ソフトウェアの品質面，安全面の信頼性が高まることが期待される．
変数の束縛機構は，プログラミング言語とくに関数型言語における基本的な研究課題であり多数の研究者により長年研究がされてきている．今年度の研究では，自由変数を含まない閉じたλ項の全体を帰納的に定義するという問題を解決することができた．この定義の方法を実装することにより，様々なメタ定理の証明が簡潔に行なえるようになることが期待できる．
またロジカル・フレームワークの基礎となるクラス理論の実装について考察を行った．その結果，クラス理論はフレーゲが『算術の基本法則』で導入した値域の概念と密接に関係することがわかった．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
変数の束縛機構に関して，自由変数を一切用いることなく，閉じたλ項を定義する方法を確立できたことは大きな収穫であった．
また，クラス理論とフレーゲの値域の概念との関連についての研究も開始することができた．
以上のことにより，研究は順調に進展していると考える．
|
| Strategy for Future Research Activity |
自由変数を用いないで閉じたλ項を定義する方法をクラス理論に導入する．これにより，メタ定理の証明がどのように簡略化できるかについて考察し，クラスのインスタンスの実現方法を検討する予定である．
ロジカル・フレームワーク実装のためのプログラミング言語の設計の詳細化を行ない予備的な実装を行なう．
|
| Causes of Carryover |
白内障手術のため26年度中に2回入院した。そのため計画していた出張を複数回中止した。
|
| Expenditure Plan for Carryover Budget |
26年度に中止した出張のための費用に充てる。
|
-
-
-
-
-
[Presentation] 計算と論理2015
Author(s)
佐藤 雅彦
Organizer
情報処理学会 第77回全国大会
Place of Presentation
京都大学
Year and Date
2015-03-17
Invited
-
[Presentation] A name-free lambda calculus2015
Author(s)
Masahiko Sato
Organizer
JAIST Logic Workshop Series 2015: Constructivism and Computablility
Place of Presentation
Shiinoki Cultural Complex, Kanazawa
Year and Date
2015-03-02 – 2015-03-06
Invited
-
