| Project/Area Number |
15300008
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Keio University |
|---|
Principal Investigator |
OKADA Mituhiro Keio University, Philosophy, Professor, 文学部, 教授 (30224025)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
KOBAYASHI Naoki Tohoku University, Graduate School of Information Sciences, Professor, 大学院・情報科学研究科, 教授 (00262155)
TERUI Kazushige National Institute of Informatics, Assistant professor, 助手 (70353422)
TAMURA Naoyuki Kobe University, Information Science and Technology Center, Professor, 学術基盤研究センター, 教授 (60207248)
|
|---|
| Project Period (FY) |
2003 – 2005
|
| Project Status |
Completed (Fiscal Year 2005)
|
| Budget Amount *help |
¥11,500,000 (Direct Cost: ¥11,500,000)
Fiscal Year 2005: ¥3,700,000 (Direct Cost: ¥3,700,000)
Fiscal Year 2004: ¥3,700,000 (Direct Cost: ¥3,700,000)
Fiscal Year 2003: ¥4,100,000 (Direct Cost: ¥4,100,000)
|
|---|
| Keywords | logical method / linear logic / formal specification / formal verification / real-time system / proof theory |
|---|
| Research Abstract |
Linear logical proof theory and semantics theory have been developed and the researches have reached a matured stage to integrate proof theory and semantics theory. In this project we developed a method of integrating proof theory and semantics of linear logic and related logics.
We specially developed a method to study proof theoretic properties using this integrated framework, by using a phase semantic techniques, including the relation between "simple logic" and linear logic, uniform and abstract characterizations of cut-eliminations and logical computation models.
We also applied the linear logical syntax and semantics to formal verification techniques on real-time system designs and correctness proof techniques on security protocols as well as to computational complexity theory and type-inference theories for programming languages.
|
