情報科学演習３ 小林研究室 課題２

並行プログラミング言語のための型システム

背景

課題１で述べたような並行プログラミング言語では、通常の ML や Haskell のような逐次プログラミング言語にはない、特有の問題が起こり得ます。たとえば、何らかの計算を行って、その結果をある通信路に一回だけ送信すべきときに、プログラマのミスや悪意により

• 送信ではなく受信を行ってしまう
• 二個以上の値を送信してしまう
• 何も送信せずに終了してしまう

内容

本課題では、上記のような問題を解決するために提案された、並行プログラミング言語のための型システムに関する論文を読んでもらい、その内容を要約・発表してもらおうと考えています。具体的には、

1. B. C. Pierce and D. Sangiorgi, "Typing and Subtyping for Mobil Processes," IEEE LICS '93, pp 376-385, 1993.
2. N. Kobayashi, B. C. Pierce, and D. N. Turner, "Linearity and the Pi-Calculus," ACM POPL '96, pp 358-371, 1996.
3. N. Kobayashi, "A Partially Deadlock-Free Typed Process Calculus," ACM TOPLAS, vol 20, no 2, pp 436-482, 1998.