1998 Fiscal Year Annual Research Report
タイプ理論及び線形論理のプログラム言語理論への応用
| Project/Area Number |
10044094
|
|---|
| Research Category |
Grant-in-Aid for international Scientific Research
|
| Section | Joint Research . |
|---|
| Research Institution | Keio University |
|---|
Principal Investigator |
岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
大堀 淳 京都大学, 数理解析研究所, 教授 (60252532)
高橋 正子 東京工業大学, 理学部, 教授 (00015588)
萩谷 昌己 東京大学, 大学院・理学系研究科, 教授 (30156252)
米澤 明憲 東京大学, 大学院・理学系研究科, 教授 (00133116)
林 晋 神戸大学, 工学部, 教授 (40156443)
|
|---|
| Keywords | タイプ理論 / 線形論理 / プログラミング言語 / プログラム意味論 / 形式的プログラム検証 / 形式的仕様 / 情報科学の論理 / 証明論 |
|---|
| Research Abstract |
現在理論情報科学界および論理学界におて注目を集めているタイプ理論及び線形論理理論を組み合わせて、新しい知的プログラミング言語の設計のための理論を確立することを目的とする。本年度は特にこの目的のための線形理論とタイプ理論の基礎研究を行った。タイプ理論はこれまでは伝統的な直観主義論理に基づいて構成され、これによってプログラムの形式仕様、プログラムの自動検証、形式仕様からのプログラムの自動抽出等の手法が確立されてきたが、基礎とする論理体系をこれまでの伝統的な直観主義論理のかわりに線形論理とすることにより、上記の種々の手法を通常のプログラム開発のみでなく、並行計算プログラムや実時間システム制御プログラム等のよりダイナミックなシステムのプログラム開発のために応用できることが明らかにされた。又、このような線形論理を用いたタイプ理論の新しい応用のために必要とされる線形論理の意味論(セマンティクス)の研究も進められ、大きな成果を得ることができた。
|
-
[Publications] M.Okada: "Phase Semantics for Higher order Completeness,cut Elimination and Normalization proofs" Theoretical Computer Science. (近刊). (1999)
-
[Publications] M.Okada-K.Terui: "The Finite Model Property for Various Fragments of Infuiticnistic Linear Logic" Journal of Symbolic Logic. (近刊). (1999)
-
[Publications] M.Okada-M.Kanovitch-A.Scedrov: "Specifying Real-Time Finite State Systems by Linear Logic" Electronic Notes of Theoretical Computer Science. 16. 1-14 (1988)
-
[Publications] M.Takahashi: "Introduction to Types and Proofs" Memoir of Math.Soc.of Japan. 2. 1-30 (1998)
-
[Publications] S.Hayashi: "Animating Proof systems" Theoretical Computer Science. (近刊). (1999)
-
[Publications] M.Sato: "Intuitionistic and Classical Natural Deduction Systems with Catch and Throw Rules" Theoretical Computer Science. (近刊). (1999)
-
[Publications] M.Takahashi-M.Okada: "Theories of Types and Proofs" Mathematical Society of Japan, 420 (1998)
-
[Publications] J.-Y.Girard-M.OKADA-A.Scedrov: "Special Volume on Linear Logic,Theoretical computer science(予定)" Elsevier Science Publishing, 462 (1999)
