Intensional models for the theory of types

Intensional models for the classical theory of types are defined and an intensional type logic, ITL is resulted. A cut-free sequent calculus for type theory is presented and the completeness of this calculus with respect to the class of intensional models through a model existence theorem is shown.