非明示的型付きデッドロックフリープロセス計算小林直樹斉藤新住井英二郎東京大学並行プログラミングより優れた表現力  既存のシステムとの合致  並列・分散環境  本質的に並列性をもつアプリケーション   ユーザ・インタフェース  シミュレーション PPL2000 Short Presentation 並列プロセス計算のモデル   計算 [Milner et al. 92] の変種：チャネル間通信に基づく並行プロセス計算       new x in P x![c].P / x?[y].P P|Q *P if x then P else Q (channel creation) (output/input) (parallel execution) (replication) (conditional branch) x![c].P | x?[y].Q → P|{c/y}Q PPL2000 Short Presentation 並行計算の表現力 2値セマフォ  関数サーバ  並行オブジェクト  PPL2000 Short Presentation 並行プログラムの安全性ネットワークからソフトウェアをダウンロード  大規模な並列･分散システムでは全体のテストが困難  → 安全性の保証が必要 PPL2000 Short Presentation 型システムによるアプローチ逐次言語に対しては成功  並行言語にはそのまま適用できない   CML の例： fun f n = let val ch = channel() in accept(ch) + n end ├ f: int -> int PPL2000 Short Presentation 型システムによるアプローチ  並行言語にはそのまま適用できない  CML の例： fun f n = let val ch = channel() in accept(ch) + n end ├ f: int -> int (f 1) → 途中で停止 PPL2000 Short Presentation 並行プログラムの安全性  例：並行プログラムが意図した動作をするか関数サーバが値を返してくるか  ロックを獲得したプロセスはいずれロックを解放するか  PPL2000 Short Presentation 既存の研究  線形チャネルプロセス計算 [Kobayashi, POPL 96]  部分的デッドロックフリープロセス計算 [Kobayashi, TOPLAS 98]  チャネル使用法計算に基づく拡張 [Sumii & Kobayashi, HLCL 98]  チャネルの使用方法を明示的にプログラマが指定 PPL2000 Short Presentation 非明示的型付けプロセス計算  構文通信にプログラマの意図を付加  new x:[]t/U in P  x!a[y].P / x?a[y].P a  {, c, o, co} x?c[y].P 成功してほしい通信 x?o[y].P いずれは実行されてほしい通信 PPL2000 Short Presentation 型推論の例  恒等関数のサーバ new f in (*f?[n,r].r![n]| new c in f![3,c].c?c[x])  関数の返り値を受け取る通信は成功してほしい  PPL2000 Short Presentation 型推論の例  恒等関数のサーバ   new f in (*f?[n,r].r![n]| new c in f![3,c].c?c[x]) 型推論 → f:[int,[int]t1/Oo]t2/(*Io|Oc) c:[int]t1/(Ic|Oo) PPL2000 Short Presentation 結論と今後の課題  結論    非明示的型付けによるデッドロックフリープロセス計算および型推論アルゴリズムを考案 SML/NJ による型検査器を実装 http://www.yl.is.s.u-tokyo.ac.jp/~shin/pub/ 課題   型システムの拡張実際の並列言語 (Pict, CML, Java) への応用 PPL2000 Short Presentation