In the past several years, the mathematical objects known as feature structures have been employed by numerous research traditions in theoretical and computational linguistics (collectively referred to as "unification-based grammar") for modeling a wide range of phenomena in the domain of natural language. The principal investigator will explore the thesis that the formalism of feature structures, appropriately extended, is capable of serving as the foundation for mathematically precise and computationally tractable theories of natural language structure that have determinate empirical consequences. The researcher would then apply such extensions to the formalization of explicit "principle-based" linguistic theories and to the construction of practical NLP programs, focussing upon such centrally important linguistic phenomena as word order, binding, long-distance dependencies ("A-bar movement"), and discourse structure. Extensions to be investigated include, inter alia, the following: (1) different varieties of negative constraints (classical negation, intuitionistic negation, and apartness); (2) different varieties of type regiments (via the logic, via structural constraints on graphs, via sorting of algebraic models) and associated inheritance schemes (inclusion polymorphism); (3) realization of such notions as list value and set value (parametric polymorphism); (4) predicates other than equality (e.g. inequality, append, subset, union) and "building-in" of equational theories (generalized unification); (5) methods for introducing recursion; (6) infinitary methods (e.g. "functional uncertainty); and (7) dynamic interpretation.