1996 Fiscal Year Final Research Report Summary
Girard's Linear Logic and its Application
| Project/Area Number |
07808035
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Keio University |
|---|
Principal Investigator |
OKADA Mitsuhiro Keio Univ.Dept.of Philosophy, Professor, 文学部, 教授 (30224025)
|
|---|
| Project Period (FY) |
1995 – 1996
|
| Keywords | Linear Logic / Phase Semantics / Concurrent Processes / Normalization / Cut-Elimination / Functional Programming / Logic Programming / Logical Computation Model |
|---|
| Research Abstract |
We established various computation models based on linear logic and their sematics. (1) In the framework of the proof-search paradigm we investigate a computation model for concurrent processes for a linear-logic based process calculus. We established semantic techniques for analysing the concurrent processes. For example, we modified the phase semantics to obtain a semantic characterization theorem for observable processes. (2) In the framework of the reduction paradigm we investigate a computation model for linear logic based typed functional programming languages. We established a new semantic framework to prove the strong normalization property. Our method is very powerful in the sense that the strong normalizability for various different logical systems are shown uniformly. (3) We applied the above semantic method to establish the semantics for Light Linear Logic, a special subsystem of Linear Logic which characterizes the polynomial-time computation. Then we investigated the polynomial computation model using this semantic framework.
|
