2015 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
クラス理論に関する研究では，クラスに適当な同値関係を導入することにより「型」をクラスとして定義可能であることがわかった．このことは事前に予想できなかった大きな収穫であった．
クラス理論とフレーゲの Sinn との関係についても新しい考察をすることができた．
以上のことにより，研究は順調に進展していると考える．
|
| Strategy for Future Research Activity |
自由変数を用いないで閉じたλ項を定義する方法をクラス理論に導入する．これにより，メタ定理の証明がどのように簡略化できるかについて考察し，クラスのインスタンスの実現方法を検討する予定である．
ロジカル・フレームワーク実装のためのプログラミング言語の設計の詳細化を行ない実装を行なう．
|
Research Products
(5 results)
-
-
-
-
-
[Presentation] 私の基礎研究2015
Author(s)
佐藤雅彦
Organizer
日本ソフトウェア科学会第32回大会
Place of Presentation
早稲田大学理工学部
Year and Date
2015-09-10
Invited
