線形論理プログラミングHACLに基づく型つき並列オブジェクト指向言語の実装

1995 Fiscal Year Annual Research Report

• Project/Area Number: 07780232
• Research Institution: The University of Tokyo
• Principal Investigator: 小林 直樹 東京大学, 大学院・理学系研究科, 助手 (00262155)
• Keywords: 並列計算 / 並列言語 / 並列オブジェクト指向 / 静的解析

Research Abstract

本年度はまず、すでに我々が提案していた線形論理に基づく並列計算の枠組であるACLを高階に拡張したHACLを提案し、その意味論・型システム等を与え、静的に型づけされた(HACLで書かれた)並列プログラムが実行時に型エラーを起こさない等の基本的な性質を証明した。また、それに基づいたインタプリタの処理系を作成して、HACLの特徴の一つである(多相型をもった)高階プロセスが非常に有効であることをプログラミングを通して確認した。
さらに、HACLの上に、インヘリタンスをはじめとする種々の機能を備えた並列オブジェクト指向言語を実現でき、かつそのようにして実現された並列オブジェクト指向言語で書かれたプログラムがHACLの型システムをとおして型推論・型チェックが行なえることを示した。その副産物として、型推論をとおして並列オブジェクトのメソッドのディスパッチが定数コストで行なえるようにコンパイルできることも示した。これらの結果に基づいて実際に、並列オブジェクト指向言語のプログラムからHACLへのトランスレータのプロトタイプも作成した。
また、HACLを含めた非同期通信に基づく並列言語の効率のよい実現のために、エフェクト解析の手法を応用した並列プログラムの通信に関する解析を行なう方法を提案し、HACLを通した定式化・基本的な性質の証明・解析システムのプロトタイプの実装を行なった。将来的にはこの静的解析システムをコンパイラに組み込み、並列プログラムの最適化コンパイルに役立てる予定である。
上記理論的側面の研究と並行してHACLに基づいた処理系の実装を進めており、現在シングルCPUのワークステーション用のコンパイラのプロトタイプがほぼ完成した状況である。

Research Products

• [Publications] Naoki Kobayashi and Akinori Yonezawa: "Asynchronous Communication Model Based on Linear Logic" Formal Aspects of Computing, Springer-Verlag. 7. 113-149 (1995)
• [Publications] Naoki Kobayashi and Akinori Yonezawa: "Static Analysis of Communication for Asynchronous Concurrent Programming Languages" In ternational Static Analysis Symposium (SAS'95), Springer-Verlag LNCS. 983. 225-242 (1995)
• [Publications] Naoki Kobayashi, Benjamin C Pierce, and David N. Turner: "Linearity and the Pi-Calculus" Proceedings of ACM SIGACT/SIGPLAN Symposium on Principles of Programming Languages (POPL'96). 358-371 (1996)