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
1:30pm
Wean 4601