• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

1997 年度 実績報告書

様相線形論理に基づく分散計算モデルおよび型システムの研究

研究課題

研究課題/領域番号 09245205
研究機関東京大学

研究代表者

小林 直樹  東京大学, 大学院・理学系研究科, 講師 (00262155)

キーワード線形論理 / 型システム / デッドロック / 分散プログラミング言語 / 並行プログラミング言語
研究概要

分散・並行プログラミング言語のさまざまな高レベル機能を柔軟に提供するためには、言語の核となる基本プリミティブを安全にかつ効率よく実現することが重要である。そこで、本研究では、そのための基礎理論の研究として、さまざまな分散言語の共通の核となる基本計算モデルの構築および、核言語レベルでの安全性の保証・最適化のためにより先進的な型システムの研究を行なった。本年度の成果は具体的には以下のとおりであり、国際会議IEEE LICS、雑誌ACM TOPLASなどで発表した。
・分散言語の核言語のモデルとしての分散並行線形論理プログラミングの提案
線形論理に場所を表す様相記号を導入することによってえられる様相線形論理の論理式(の一部)と分散並行プロセスとが対応することに着目し、分散並行線形論理プログラミングの枠組を定式化した。特に、場所に依存する変数の束縛環境の構築/参照、計算の実行場所の指定などの分散言語特有の機能が、様相記号を用いて統一的に表現できることを示した。
・デッドロックフリーダムや決定性を保証する並行言語の型システムの洗練・一般化
我々が以前から開発を進めてきた、並行プログラムのデッドロックフリーダムなどを保証できる型システムを洗練化し、それを用いて、関数の並列評価プリミティブや並行オブジェクトを用いたプログラムのデッドロックフリーダムを保証できることを示し、型チェッカを実現した。さらにその一般化を行い、より広範囲の並行プログラムのデッドロックフリーダム性を扱うことができるようにするとともに、並行プログラムの最適化にも応用できることを示した。

  • 研究成果

    (4件)

すべて その他

すべて 文献書誌 (4件)

  • [文献書誌] Naoki Kobayashi: "A Partially Deadlock-free Typed Process Calculus" Proceedings of 12th Annual IEEE Symposium on Logic in Computer Science(LICS'97). 128-139 (1997)

  • [文献書誌] Naoki Kobayashi: "A Partially Deadlock-free Typed Process Calculus" ACM Transactions on Programming Languages. (印刷中). (1998)

  • [文献書誌] A.Igarashi and N.Kobayashi: "Type-Based Analysis of Usage of Communication Channels for Concurrent Programming Languages" Proceedings of SAS'97(Springer Lecture Notes in Computer Science). 1302. 187-201 (1997)

  • [文献書誌] 清水智弘,小林直樹: "分散並行線形論理プログラミング" 日本ソフトウェア科学会第14回大会論文集. 305-308 (1997)

URL: 

公開日: 1999-03-15   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi