プログラミング言語には、実行前にプログラム中の誤り検査を行う静的型付言語と実行中に検査を行う動的型付言語があり一長一短があることが知られている。本研究では両方の機能を兼ね備えたプログラミング言語を設計し、その理論と実装手法を研究した。理論的成果として、部分的に型付けされるプログラムの実行前検査のためのアルゴリズムと実行時検査手法を与え、アルゴリズムの正当性や、その検査で検出される誤りは全て実行前検査を行わなかった部分に起因することを証明した。また実行時検査の実装手法を考案した。