Metalanguages that are suitable for implementing derivation systems such as proof systems and program transformation systems will be investigated. A crucial feature of such languages appears to be the ability to represent higher.order objects and to manipulate them in logically meaningful ways. A higher.order logic programming language that provides such a capability will be studied. This language provides simply typed -terms as data structures for representing objects such as programs and proofs and incorporates higher-order unification and search primitives for reasoning about such objects. Experiments have shown that such a language has considerable potential as a metalanguage, thus pointing to the importance of a robust and efficient implementation for it. This research will examine techniques for efficiently implementing the novel operations in this language, i.e. higher-order unification and the new search primitives, resulting in the design of an abstract machine. An implementation will be provided based on these results and will be used to explore applications of this language within actual derivation systems. Feedback from these studies will be used to improve the behavior of the implementation on commonly occurring problems. Extensions to the language based on using a richer class of -terms will also be addressed.
