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
|
| Project Status |
Completed (Fiscal Year 1996)
|
| Budget Amount *help |
¥2,100,000 (Direct Cost: ¥2,100,000)
Fiscal Year 1996: ¥1,100,000 (Direct Cost: ¥1,100,000)
Fiscal Year 1995: ¥1,000,000 (Direct Cost: ¥1,000,000)
|
|---|
| Keywords | Linear Logic / Phase Semantics / Concurrent Processes / Normalization / Cut-Elimination / Functional Programming / Logic Programming / Logical Computation Model / Phase Semantics / 証明論 / 正規化定性 / プログラミング言語 |
|---|
| 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.
|
Report
(3 results)
Research Products
(31 results)
