| 研究課題/領域番号 |
10044094
|
|---|
| 研究種目 |
国際学術研究
|
| 応募区分 | 共同研究 |
|---|
| 研究機関 | 慶応義塾大学 |
|---|
研究代表者 |
岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
|
|---|
| 研究分担者 |
大堀 淳 京都大学, 数理解析研究所, 教授 (60252532)
高橋 正子 東京工業大学, 理学部, 教授 (00015588)
萩谷 昌己 東京大学, 大学院・理学系研究科, 教授 (30156252)
米澤 明憲 東京大学, 大学院・理学系研究科, 教授 (00133116)
林 晋 神戸大学, 工学部, 教授 (40156443)
|
|---|
| キーワード | タイプ理論 / 線形論理 / プログラミング言語 / プログラム意味論 / 形式的プログラム検証 / 形式的仕様 / 情報科学の論理 / 証明論 |
|---|
| 研究概要 |
現在理論情報科学界および論理学界におて注目を集めているタイプ理論及び線形論理理論を組み合わせて、新しい知的プログラミング言語の設計のための理論を確立することを目的とする。本年度は特にこの目的のための線形理論とタイプ理論の基礎研究を行った。タイプ理論はこれまでは伝統的な直観主義論理に基づいて構成され、これによってプログラムの形式仕様、プログラムの自動検証、形式仕様からのプログラムの自動抽出等の手法が確立されてきたが、基礎とする論理体系をこれまでの伝統的な直観主義論理のかわりに線形論理とすることにより、上記の種々の手法を通常のプログラム開発のみでなく、並行計算プログラムや実時間システム制御プログラム等のよりダイナミックなシステムのプログラム開発のために応用できることが明らかにされた。又、このような線形論理を用いたタイプ理論の新しい応用のために必要とされる線形論理の意味論(セマンティクス)の研究も進められ、大きな成果を得ることができた。
|
