1995 Fiscal Year Annual Research Report

タイプ理論及び線形論理のプログラム言語理論への応用

Research Project

Project/Area Number	07044093
Research Institution	Keio University
Principal Investigator	岡田光弘慶応義塾大学, 文学部, 助教授 (30224025)
Co-Investigator(Kenkyū-buntansha)	林普神戸大学, 理工学部, 教授 (40156443) 高橋正子東京工業大学, 理学部, 助教授 (00015588) 大堀淳京都大学, 数理解析研, 助教授 (60252532) 萩谷昌巳東京大学, 理学系研究科, 教授 (30156252) 佐藤雅彦東北大学, 電通研, 教授 (20027387)
Keywords	線形論理 / タイプ理論 / プログラム言語
Research Abstract	タイプ理論と線形論理を用いた新しいマルチパラダイムプログラム言語の設計のための基礎理論を与えることを本年度の主な目的とした。この目的のために特に、Phase Semantics及びCoherence Semantics等の線形論理の基本的なSemantics理論の整備をするとともに、それらのSemantics理論のタイプ付高階プログラミング言語理論への応用を与えた。特に、CDherence Semanticsは、我々の線形論理に基づいたタイプ付プログラミング言語において、Denotational Semanticsとしての役割を果たすものであり、又Phase Semanticsは、これまで考えられてきたように単に証明可能性概念に対する完全性を与えるだけではなく、証明概念自身についての完全性も与えることが示された。特に、後者の考え方から、Phase Semanticsを用いた証明の正規化定理の証明が得られることが示された。証明の正規化はタイプ付プログラミング言語の計算モデルを与えることから、上記のPhase Semantics理論は、我々のマルチパラダイムプログラミング言語の計算モデルの基礎となることが示された。一方、線形論理を基にした並行計算モデルの定式化、及びInteraction Nets及びProof netsの理論が与えられた。これらは線形論理による並行計算及び (ラムグ計算等の) sequentialな計算の分析手法を与えるものであり、これらの理論を我々のマルチパラダイム言語に内臓することにより、我々のマルチパラダイム言語が、並行計算プログラムや計算処理のコントロールに非常に適したものとなることが示された。

Research Products

(10 results)

All Other

All Publications (10 results)

[Publications] Jouannaud,Jean-Pierre 岡田光弘: "Abstract Data Type Systems" Theoretical Computer Science. (近刊). (1996)
[Publications] 岡田光弘(浜野と共著): "A Direct Proof of Buchholz's Hydra Game" Archiev for Mathematical Logic. (近刊). (1996)
[Publications] Susumu Hayashi(林晋)and S.Kobayashi: "A new formalization of Feferman's system of functions and classes and its velation to Frege structure." International J. of Foundations of Computer Science.6(No.3). 187-202 (1995)
[Publications] M.Hagiya et al.: "Formalization of Planar Graphs" Proc.of Higher Order Theorem Proving and its Applications,Lecture Notes in Computer Science(Springer). 971. 369-384 (1995)
[Publications] M.Takahashi: "Parallel reduction in λ-calculus" Information and Computation. 118. 120-127 (1995)
[Publications] 佐藤雅彦(亀山との共著): "自己反映的証明体系RPTの理論と実現" コンピュータソフトウエア. 12(2). 32-51 (1995)
[Publications] 岡田光弘: "情報科学のための論理" 産業図書, 240 (1996)
[Publications] Girard,Jean-Yves 岡田光弘 Scedrov,Andre: "Special Issue on Linear Logic (ENTCS series)" Elsevier社(オランダ), 420 (1996)
[Publications] Girard,Jean-Yves(フランス側代表者): "Advances in Linear Logic" Cambridge University Press, 340 (1995)
[Publications] 林普: "プログラム検証論" 共立出版, 208 (1995)

1995 Fiscal Year Annual Research Report

タイプ理論及び線形論理のプログラム言語理論への応用

Principal Investigator

岡田 光弘 慶応義塾大学, 文学部, 助教授 (30224025)

Research Products

[Publications] Jouannaud,Jean-Pierre 岡田光弘: "Abstract Data Type Systems" Theoretical Computer Science. (近刊). (1996)

[Publications] 岡田光弘(浜野と共著): "A Direct Proof of Buchholz's Hydra Game" Archiev for Mathematical Logic. (近刊). (1996)

[Publications] Susumu Hayashi(林晋)and S.Kobayashi: "A new formalization of Feferman's system of functions and classes and its velation to Frege structure." International J. of Foundations of Computer Science.6(No.3). 187-202 (1995)

[Publications] M.Hagiya et al.: "Formalization of Planar Graphs" Proc.of Higher Order Theorem Proving and its Applications,Lecture Notes in Computer Science(Springer). 971. 369-384 (1995)

[Publications] M.Takahashi: "Parallel reduction in λ-calculus" Information and Computation. 118. 120-127 (1995)

[Publications] 佐藤雅彦(亀山との共著): "自己反映的証明体系RPTの理論と実現" コンピュータソフトウエア. 12(2). 32-51 (1995)

[Publications] 岡田光弘: "情報科学のための論理" 産業図書, 240 (1996)

[Publications] Girard,Jean-Yves 岡田光弘 Scedrov,Andre: "Special Issue on Linear Logic (ENTCS series)" Elsevier社(オランダ), 420 (1996)

[Publications] Girard,Jean-Yves(フランス側代表者): "Advances in Linear Logic" Cambridge University Press, 340 (1995)

[Publications] 林普: "プログラム検証論" 共立出版, 208 (1995)

岡田光弘慶応義塾大学, 文学部, 助教授 (30224025)