「並行プログラミング言語へのチャネル使用法宣言の導入」［論文誌Vol.48, No.SIG10(PRO33), pp. 101-113(2007)］

［論文概要］
　並行プログラムのデッドロック等の性質の検証のため，使用法表現という通信チャネルの使われ方を表す式を型推論によって求める枠組みが小林らによって提案されている．本研究では，使用法表現をプログラマが宣言できるようにこの型システムを拡張することで，通信がプログラマの意図どおりに行われるかどうかを静的に検証できるようにする．拡張に当たっての主な課題は，使用法表現間の部分型関係判定アルゴリズムの構築である．部分型関係は一般に決定不能であるため，宣言できる使用法を制限し，部分型関係判定問題をペトリネットの到達可能性判定問題に帰着する．

［推薦理由］
　並行プログラムの通信チャネルが正しく使われているかを型によって判定する方法を提案している．この型は単に送受信されるデータの型のみではなく，チャネルが送受信に使われる回数なども指定することができる．これにより，システムの動作を静的に検証することが可能になる．本論文では，チャネルの使用方法の表現力が従来よりも高くなっており（正規言語から決定性ペトリネット言語に拡張されている），その判定アルゴリズムをペトリネットの到達可能性問題に帰着するなど，十分な新規性がある．また，この型検査アルゴリズムを並行プログラミング言語Pictに試験的に実装するなど，今後実際の並行プログラムの検証への適用が期待できる．理論的にも実用的にも興味深く，論文賞に値する論文である．