| Project/Area Number |
10139237
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research on Priority Areas (A)
|
| Allocation Type | Single-year Grants |
|---|
| Research Institution | Keio University |
|---|
Principal Investigator |
岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
|
|---|
| Project Period (FY) |
1998
|
| Project Status |
Completed (Fiscal Year 1998)
|
| Budget Amount *help |
¥1,400,000 (Direct Cost: ¥1,400,000)
Fiscal Year 1998: ¥1,400,000 (Direct Cost: ¥1,400,000)
|
|---|
| Keywords | タイプ理論 / 項書き換え系 / タイプ推論 / Inductive Types / 停止性 / 並行計算 / 高階関数 / 構成論理 |
|---|
| Research Abstract |
昨年までに確立した融合言語の計算モデル〔これは構成論理と頭書き換え系との両停止性証明(強制規化定理証明)を融合して得られた〕に基づいて、マルチパラダイム・プログラミング方法論の開発を行った。特に、昨年度までに与えたInductive Type推論機構をさらに強めることによって、より一般的なInductive Type推論を我々の融合言語の中で供給できることとなった。また、それに合わせたrecursors等の高階関数定義の枠組の拡張がなされ、これによって高階関数の使用に関して、項書換え(代数的仕様)パラダイムとタイプ理論パラダイムを融合した新しいプログラミング方法論が導入された。
他方、項書き換えパラダイムを、伝統的な項書き換え系のかわりに、並行書き換え処理を遂行うるマルチセット書き換え系(しばしば、並行項書き換え系とも呼ばれる)を利用して拡張することにより、我々の融合言語の枠組が、並行計算プログラミングや実時間システムのプログラミングに適していることも示された。
|
