並行計算モデルであるJoin算法の記述法をJAVAに組み込んでスレッドプログラ ミングを容易にすることを目的としてプログラミング言語JoinJAVAが設計され， そのコンパイラが開発されている．Join 算法には型推論システムが定式化され ており，与えられたJoin算法プログラムの型推論が成功すれば，そのプログラ ムの実行時に型不整合が生じないことが保証される．しかしながら，JoinJAVA コンパイラにはJoin算法記述部分についての型推論が実装されていない．本研 究の目的は，Join 算法の型推論を実現し，JoinJAVAコンパイラに組み込むこと である．
Join算法の型推論システムは型判定式を推論する規則の集合からなり，その推 論を行うアルゴリズムを開発することは容易ではない．本研究のアイデアは， Join算法の型推論を関数型プログラミング言語SMLの型推論に帰着することであ る．すなわち，Join算法プログラムJを次のようなSMLプログラムM に変換する．Jの型推論が成功するときかつそのときに限り，Mの型推論が成功 する．SMLの型推論はSMLインタプリターで行えるから， Join算法プログラムの型推論は次のようにして行える．まず本論文の変換を用 いてJoin算法プログラムSMLプログラムに変換し，得られたSMLプログラムをSML イタプリタにロードする．ロードした結果，型エラーがあれば元のJoin算法プ ログラムにも型エラーが存在する．型エラーが無ければ元のJoin算法プ ログラムは型不整合を生じないと判定できる．
またこの変換が健全であること，すなわち， MのSMLにおける型推論が 成功するならば，Jの型推論も成功することを証明した．