Application of Logic to Programming Language Theory
| Project/Area Number |
05808030
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Keio University, Faculty of Letters |
|---|
Principal Investigator |
OKADA Mitsuhiro Keio University, Dept.of Philosophy, Associate Professor., 文学部, 助教授 (30224025)
|
|---|
| Project Period (FY) |
1993 – 1994
|
| Project Status |
Completed (Fiscal Year 1994)
|
| Budget Amount *help |
¥1,900,000 (Direct Cost: ¥1,900,000)
Fiscal Year 1994: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 1993: ¥1,000,000 (Direct Cost: ¥1,000,000)
|
|---|
| Keywords | Multi-paradigm programming / Higher order term rewriting / Proof theory / Algebraic specification / Type theory / Typed lambda calculus / Termination problem / Mobile linear logic / 項書き換えシステム / 高階等式言語 / 論理的プログラム言語 / プログラム検証 |
|---|
| Research Abstract |
We established a logical computation model for a multi-paradigm programming language which combines the two programming paradigms, that for polymorphic typed fanctional language and that for algebraic (equational) specification language. For that purpose, we combined the two logical computation models, polymorphically typed lambda calculus on one hand a higher order and first order term rewrite system on the other hand. In particular, we established a termination criterion and a confluence criterion for the combined computation model. We also implemented the resulting combined programming language.
We also studied mobile linear logic, which is an extension of the usual linear logic, in order to capture the paradigm of higher order concurrent programming. Here, our mobile linear logic has the expressive power of Milner's pi-calculus (a calculus for concurrency systems with mobile message passings) and its natural extension (with higher order mobile message passings). The higher order (strong) mobile message passing mechanism was realized by the logical language with self-referential predicates. Such a logical language was introduced by restricting the use of higher order abstract terms, which avoided Russell's paradox even though some sort of self-referential predicates was permitted.
|
Report
(2 results)
Research Products
(22 results)
