This book develops the theory of typed feature structures, a data structure that generalizes both first-order terms and feature structures of unification-based grammars to include inheritance, typing, inequality, cycles, and intensionality.