Towards Practical Higher-Order Metalanguages

Investigations will be conducted on the implementation and use of a higher-order metalanguage that has several applications in prototyping derivation systems. This metalanguage is based on the logic programming paradigm but it enriches conventional such languages by incorporating a polymorphic typing regimen, providing the terms of a lambda calculus as data structures, using higher- order unification for probing these data structures and including two new search primitives for realizing hypothetical reasoning and for creating new constants during search. The implementation problems that are raised by each of these features have been studied and a preliminary abstract machine has been designed for the underlying logical language. Efforts will now be devoted to a practical realization of a programming system based on these ideas. Language and interface design aspects will be considered to enhance the usability of the metalanguage based on the logical language. The abstract machine will be extended to cover the additional language features and an implementation of the overall system will be undertaken. Experiments will be conducted with the implementation to obtain feedback on specific design decisions pertaining to the abstract machine. Attempts will be made to tailor the implementation to sublanguages that are becoming of independent interest. Theoretical issues affecting the quality and correctness of the implementation will also be examined. A particular interest will be the study of notations for lambda terms and their relevance to optimality in reduction.