Formation rules are presented for an W-order logic with lambda operator in which each term has a well defined type. Transformation rules are given defining lambda-conversion, special conversion, substitution, and alphabetic change of bound variables. The notion of one term being an 'instance' of another is then defined using these transformation rules. The main problem of the paper is to develop a 'matching procedure' for pairs of terms, so that every common instance of the two given terms is an instance of some term produced by the matching procedure. This is accomplished by analysing the terms according to the formation rules, matching the outermost parts first, then proceeding inductively inward. Examples are given to show that an infinite set of terms may be needed for this purpose. Conditions under which such an infinite set is needed are discussed. A procedure is developed for producing at least one common instance, if one exists.