Gopalan Nadathur

Issues in the Design and Implementation of a Higher-Order Metalanguage

The manipulation of syntactically complex objects like programs, formal specifications, mathematical expressions, types and proofs is of interest in systems such as compilers, interactive theorem provers, symbolic computation systems, type checkers, program transformers and generic derivation systems. The prototyping and implementation of such systems can be simplified by the availability of a programming language, referred to as a metalanguage, that permits flexible representations of the relevant objects and that contains mechanisms useful in reasoning about these objects. Logic programming languages provide a good basis for such a metalanguage because of the support they offer for rule based specifications and for unification and search that are useful in obtaining implementations from such specifications. However, certain enhancements must be made to usual logic programming languages in order to produce a metalanguage that is of general interest. These enhancements include the provision of lambda terms for representing objects by means of their higher-order abstract syntax and mechanisms for controlling the availability and attributes of objects in subparts of a reasoning process. Such additions have been considered in our work and have resulted in a language called lambda Prolog. In this talk we will discuss the new features from the perspective of metalanguage applications and we will outline approaches to their efficient implementation. The ideas that are to be presented are embedded in an abstract machine and compiler based implementation of lambda Prolog that will also be discussed.
December 1, 1998
Wean 4601