条件付き項書換え系は、書換え規則に書換えを行う為に満たす必要がある 条件が付随する項書換え系であり、種々のシステムを記述するのに適している。 一方で、型の整合性をチェックする役割を持つプログラムの型検査や、 型が指定されていない部分プログラムの型を推論する型推論に基礎を与える型シ ステムの推論規則は一般に条件付の推論規則で与えることが出来る。 従って、プログラミング言語の型検査と型推論に条件付項書換え系を利用す ることが可能である。 本研究では、条件付項書換え系の実行系を実現するとともに、 簡単なプログラミング言語を取り上げて、型システムを条件付項書換え系で表し、 条件付項書換え系の実行系を用いて、任意に与えられたプログラムの型を 推論するシステムを実現する。