9803971 Many reasoning and specification tasks require the analysis of logically complex syntactic objects. Such tasks arise, for instance, in using typing systems, in describing and prototyping programming languages, in effecting program transformations, in demonstrating program correctness, in realizing theorem provers, in describing the semantics of natural languages and in constructing corresponding parsers for them. A satisfactory framework for performing such tasks is obtained from using lambda- terms to represent the objects that are of interest and a constructive logic to describe their properties. This research addresses questions of implementation and use of lambda Prolog, a programming language that provides such a framework. The starting point for this work is an implementation of lambda Prolog that embodies the first serious attempt to realize many of its new features in an efficient manner. Using this system, the project conducts an extensive empirical study of the impact on efficiency of choices in the representation of lambda terms and in the compilation of unification and other operations on these terms. Refinements to the structure of lambda terms and to other language features are considered towards understanding the tradeoffs between efficiency and expressiveness. Issues relevant to constructing a flexible programming system around the language are studied. Finally, the strength of the programming system and of the methods supported by it are tested by employing them to implement a compiler for lambda Prolog.***
