| Project/Area Number |
10044094
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (A).
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Keio University |
|---|
Principal Investigator |
OKADA Mitsuhiro Keio Univ., Dept. of Philosophy, Professor, 文学部, 教授 (30224025)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
HAGIYA Masami Tokyo Univ., Dept. of Comp. Sci., Professor, 大学院・理学研究科, 教授 (30156252)
YONEZAWA Akinori Tokyo Univ., Dept. of Comp. Sci., Professor, 大学院・理学研究科, 教授 (00133116)
HAYASHI Susumu Kobe Univ., Dept. of Syst. Eng., Professor, 工学部, 教授 (40156443)
OHORI Atsushi Kyoto Univ., RIMS, Professor, 数理解析研究所, 教授 (60252532)
TAKAHASHI Masako Tokyo Ins. Tech., Dept. of Comp. Sci., Professor, 理学部, 教授 (00015588)
|
|---|
| Project Period (FY) |
1998 – 1999
|
| Project Status |
Completed (Fiscal Year 1999)
|
| Budget Amount *help |
¥9,500,000 (Direct Cost: ¥9,500,000)
Fiscal Year 1999: ¥4,400,000 (Direct Cost: ¥4,400,000)
Fiscal Year 1998: ¥5,100,000 (Direct Cost: ¥5,100,000)
|
|---|
| Keywords | Type Theory / Linear Logic / Functional Language / Programming Language / Proof Theroy / Formal specification / Formal Verification / Real Time System / プログラミング言語 / プログラム意味論 / 形式的プログラム検証 / 形式的仕様 / 情報科学の論理 |
|---|
| Research Abstract |
Our purpose of the research was applications of type theory, intuitionistic logic and linear logic to programming language theory. We first gave various fundamental researches of semantics and the proof-normalization and proof-search techniques for type theory (equivalently, intuitionistic logic, under the Curry-Howard correspondence) and linear logic, which provided computation models of our new programming and specification/verification languages. In particular, we gave a logical computation model for a combined language of type theory with linear logic, which resulted in a new multi-paradigm programming language with both the paradigm of typed functional programming language and the paradigm of concurrent process calculus. We also gave computation models for proof-search based-verification systems, including verification systems for concurrent process specification languages and for real-time multi-agent system specification languages. In particular, we gave PSPACE-decidability result for verifications of safety and other important properties of real-time finite state system specifications based on our linear logic-based formal specification language.
|
