2000 Fiscal Year Annual Research Report
並行・分散計算の先進的理論に基づく分散プログラミング言語処理系の構築
| Project/Area Number |
10558040
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
小林 直樹 東京工業大学, 大学院・情報理工学研究科, 助教授 (00262155)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
登内 敏夫 日本電気(株), C&Cメディア研究所, 担当研究員(研究職)
五十嵐 淳 東京大学, 大学院・総合文化研究科, 助手 (40323456)
米澤 明憲 東京大学, 大学院・理学系研究科, 教授 (00133116)
|
|---|
| Keywords | オブジェクト指向 / Java / 分散プログラミング言語 / 並行プログラミング言語 / 型推論 / 型システム / デッドロック / プロセス計算 |
|---|
| Research Abstract |
本研究では、最新の基礎理論・実装技術に基づき、安全かつ効率の良い分散・並行プログラミング言語を再設計・実装することを目的とする。本年度の成果は以下のとおり。
1.オブジェクト指向部分の言語設計をすすめるため,既存の言語Javaやその拡張の中の重要な機能である仮想型,内包クラスの定式化を行い,これらの機能がより単純な機能だけからなる言語上で実現できることを示すとともにその実現方式の正当性の証明も行った.これにより、核となる分散言語上に上記のような高レベルなオブジェクト指向の機能を正しく実現する手法が確立された.
2.並行・分散プログラムの安全性を保証するため,これまでに考案してきたデッドロックフリーダムを保証する型システムをさらに改良,拡張し,並行・分散プログラム中の特定の通信が(プログラム全体が停止しない場合でも)有限時間内,あるいは与えられた計算ステップ数内にいずれ必ず成功することを保証する型システムの構築に成功した.
3.前年度までに構築したデッドロックフリーダムを保証する型システムおよび型推論アルゴリズムの有効性を検証するため,その型システムに基づくデッドロックの解析器を実用的並行プログラミング言語であるCMLに組み込む作業に着手した.その過程で,多相型およびレコード型の導入など実際の言語に適用する上で必要となる型システムの拡張についても研究を行った.
4.これまでに研究を行ってきた型システムはデッドロック,レース条件など個別の性質を検証するためのものであったが,現実のプログラミング言語に組み込むためには一つの型システムでそれらの性質を包括的に扱うことが望ましい.そこで,並行プログラミング言語の標準的計算モデルであるπ計算を対象とし,種々の性質を統一的に扱うことのできる型システムを考案した.
|
Research Products
(6 results)
-
[Publications] A.Igarashi and N.Kobayashi: "Type Reconstruction for Linear Pi-Calculus with I/O Subtyping"Information and Computation. 161. 1-44 (2000)
-
[Publications] Naoki Kobayashi: "Type Systems for Concurrent Processes : From Deadlock-Freedom to Livelock-Freedom, Time-Boundedness"Proceedings of IFIP TCS2000, Springer LNCS. 1872. 365-389 (2000)
-
[Publications] N.Kobayashi,S,Saito,and E.Sumii: "An Implicitly-Typed Deaklock-Free Process Calculus"Proceedings of CONCUR2000, Springer LNCS. 1877. 489-503 (2000)
-
[Publications] A.Igarashi and N.Kobayashi: "A Generic Type System for the Pi-Calculus"Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages(POPL2001). 128-141 (2001)
-
[Publications] A.Igarashi and B.C.Pierce: "Foundations for Virtual Types"Information and Computation. (印刷中). (2000)
-
[Publications] A.Igarashi and B.C.Pierce: "On Inner Classes"Information and Computation. (印刷中). (2000)
