课题基金 / 基金详情

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

様相線形論理に基づく分散計算モデルおよび型システムの研究
基于模态线性逻辑的分布式计算模型与类型系统研究
批准号：
09245205
负责人：
小林 直樹
金额：
$0.77万
依托单位：
The University of Tokyo
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research on Priority Areas
财政年份：
1997
资助国家：
日本
项目状态：
已结题
起止时间：
1997 至 --
来源：
https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-09245205/
关键词：
線形論理型システムデッドロック分散プログラミング言語並行プログラミング言語

项目摘要

项目成果

小林 直樹的其他基金

相似基金

相关文献

中文摘要
翻译
分散・並行プログラミング言語のさまざまな高レベル機能を柔軟に提供するためには、言語の核となる基本プリミティブを安全にかつ効率よく実現することが重要である。そこで、本研究では、そのための基礎理論の研究として、さまざまな分散言語の共通の核となる基本計算モデルの構築および、核言語レベルでの安全性の保証・最適化のためにより先進的な型システムの研究を行なった。本年度の成果は具体的には以下のとおりであり、国際会議IEEE LICS、雑誌ACM TOPLASなどで発表した。・分散言語の核言語のモデルとしての分散並行線形論理プログラミングの提案線形論理に場所を表す様相記号を導入することによってえられる様相線形論理の論理式(の一部)と分散並行プロセスとが対応することに着目し、分散並行線形論理プログラミングの枠組を定式化した。特に、場所に依存する変数の束縛環境の構築/参照、計算の実行場所の指定などの分散言語特有の機能が、様相記号を用いて統一的に表現できることを示した。・デッドロックフリーダムや決定性を保証する並行言語の型システムの洗練・一般化我々が以前から開発を進めてきた、並行プログラムのデッドロックフリーダムなどを保証できる型システムを洗練化し、それを用いて、関数の並列評価プリミティブや並行オブジェクトを用いたプログラムのデッドロックフリーダムを保証できることを示し、型チェッカを実現した。さらにその一般化を行い、より広範囲の並行プログラムのデッドロックフリーダム性を扱うことができるようにするとともに、並行プログラムの最適化にも応用できることを示した。
英文摘要
分散・並行プログラミング言語のさまざまな高レベル機能を柔軟に提供するためには、言語の核となる基本プリミティブを安全にかつ効率よく実現することが重要である。そこで、本研究では、そのための基礎理論の研究として、さまざまな分散言語の共通の核となる基本計算モデルの構築および、核言語レベルでの安全性の保証・最適化のためにより先進的な型システムの研究を行なった。本年度の成果は具体的には以下のとおりであり、国際会議IEEE LICS、雑誌ACM TOPLASなどで発表した。・分散言語の核言語のモデルとしての分散並行線形論理プログラミングの提案線形論理に場所を表す様相記号を導入することによってえられる様相線形論理の論理式(の一部)と分散並行プロセスとが対応することに着目し、分散並行線形論理プログラミングの枠組を定式化した。特に、場所に依存する変数の束縛環境の構築/参照、計算の実行場所の指定などの分散言語特有の機能が、様相記号を用いて統一的に表現できることを示した。・デッドロックフリーダムや決定性を保証する並行言語の型システムの洗練・一般化我々が以前から開発を進めてきた、並行プログラムのデッドロックフリーダムなどを保証できる型システムを洗練化し、それを用いて、関数の並列評価プリミティブや並行オブジェクトを用いたプログラムのデッドロックフリーダムを保証できることを示し、型チェッカを実現した。さらにその一般化を行い、より広範囲の並行プログラムのデッドロックフリーダム性を扱うことができるようにするとともに、並行プログラムの最適化にも応用できることを示した。
期刊论文(4)
专著(0)
科研奖励(0)
会议论文
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)
A.Igarashi 和 N.Kobayashi：“基于类型的并发编程语言通信通道使用情况分析”SAS97 论文集（计算机科学中的施普林格讲义）。
DOI： --
发表时间：
期刊：
影响因子： --
作者： []
通讯作者：
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：“部分无死锁类型化过程演算”第 12 届 IEEE 计算机科学逻辑研讨会论文集 (LICS97)。
DOI： --
发表时间：
期刊：
影响因子： --
作者： []
通讯作者：
Naoki Kobayashi: "A Partially Deadlock-free Typed Process Calculus" ACM Transactions on Programming Languages. (印刷中). (1998)
Naoki Kobayashi：“部分无死锁的类型化过程演算”ACM 编程语言汇刊（正在出版）。
DOI： --
发表时间：
期刊：
影响因子： --
作者： []
通讯作者：
清水智弘,小林直樹: "分散並行線形論理プログラミング" 日本ソフトウェア科学会第14回大会論文集. 305-308 (1997)
Tomohiro Shimizu、Naoki Kobayashi：“分布式并行线性逻辑编程”日本软件学会第 14 届年会论文集 305-308 (1997)。
DOI： --
发表时间：
期刊：
影响因子： --
作者： []
通讯作者：
無住道暁と南宋代成立典籍に関する総合的研究
  • 批准号：
    23K00298
  • 项目类别：
    Grant-in-Aid for Scientific Research (C)
  • 资助金额：
    $1.41万
  • 财政年份：
    2023
  • 负责人：
    小林 直樹
  • 依托单位：
    Osaka Metropolitan University
潜在的カビ毒産生菌種を利用したカビ毒生合成抑制メカニズムの解明
  • 批准号：
    23K05081
  • 项目类别：
    Grant-in-Aid for Scientific Research (C)
  • 资助金额：
    $2.91万
  • 财政年份：
    2023
  • 负责人：
    小林 直樹
  • 依托单位：
    Azabu University
偏光分光型マルチスペクトルカメラを用いた目視診断用画像システムの研究開発
  • 批准号：
    23K11878
  • 项目类别：
    Grant-in-Aid for Scientific Research (C)
  • 资助金额：
    $3.08万
  • 财政年份：
    2023
  • 负责人：
    小林 直樹
  • 依托单位：
    Saitama Medical University
Program Verification Based on Higher-Order Fixpoint Logic
  • 批准号：
    20H00577
  • 项目类别：
    Grant-in-Aid for Scientific Research (A)
  • 资助金额：
    $28.45万
  • 财政年份：
    2020
  • 负责人：
    小林 直樹
  • 依托单位：
    The University of Tokyo
海外基金