This is a detailed study of the logic and complexity of type inference, with applications to functional and logic programming languages. The typed lambda calculus provides a functional "simplest" such language for this research. Computation can be embedded in type disciplines for this language, and complexity results concerning the decision process of typability can be derived for natural extensions to the language, including ML-style let-polymorphism, fixed point operators, and second-order polymorphic lambda calculus. Other complex forms of typing will be analyzed, complexity- and unification- related models of computation. The phenomenon of boundedness in database logic programs, and the relationship between deciding typability and actually computing types will be studied.
