Summary: Equational type logic is an extension of (conditional) equational logic that enables one to deal in a single, unified framework with diverse phenomena such as partiality, type polymorphism and dependent types. In this logic, terms may denote types as well as elements, and atomic formulae are either equations or type assignments. Models of this logic are type algebras, viz. universal algebras equipped with a binary relation - to support type assignment. Equational type logic has a sound and complete calculus, and initial models exist. The use of equational type logic is illustrated by means of simple examples, where all of the aforementioned phenomena occur. Formal notions of reduction and extension are introduced, and their relationship to free constructions is investigated. Computational aspects of equational type logic are investigated in the framework of conditional term rewriting systems, generalizing known results on confluence of these systems. Finally, some closely related work is reviewed and future research directions are outlined in the conclusions.