The use of type constraints in programming language can improve programming style and program reliability. There are several researches to provide Prolog with type system, and Mycroft et al. proposed a polymorphic type system for Prolog based on type declaration [MyOk84]. However their system has some incorrect points in the definition of well-typing of Prolog programs. Moreover, the definition of well-typing is so restrictive that many useful programs can not be defined to be well-typed by their definition.
In this thesis, their definition is modified to be correct and extended to use mode information for the type system to be more expressive. In addition, an algorithm for the static type checking of this extention of typed Prolog is provided and proved to be sound, which means that a well-typed program does not allow any run-time type error.
