構成的型理論はCurry-Howardの同型対応により論理体系に対応している。 プログラムの仕様を記述するための十分な表現力を持つ論理体系に対応す る型理論では、プログラムの仕様を型を用いて形式的に記述することがで きる。ある変数がこの仕様を表す型の要素であるという判定を構成的型理 論のもとで成り立つかを証明できれば、証明から具体的なプログラムを抽 出でき、結果的にプログラムを合成する事が可能となる。
本研究では、構成的型理論の一つであるMartin-Löfの型理論を、プロ グラム合成に適した形に拡張し、この型理論に基づくプログラム合成系を 計算機上に実装する。実装にはStandard ML(以下SML)を用いる。そして、 合成された型理論のプログラムからSMLのプログラムへの変換手続きを提案 し、型理論で記述された仕様からSMLのプログラムが合成可能であることを 例を用いて示す。最後に、Martin-Löfの型理論に基づく他のシステム と本研究で実装したプログラム合成系について比較、検討する。