Amy Felty. Presented at the 1993 International Symposium on Logic Programming, October 1993.

**Abstract:**
The higher-order logic programming language lambda Prolog contains
the simply-typed lambda-terms as its basic data structures. These
terms can be used to elegantly express the *higher-order abstract
syntax* of objects that include notions of bound variables such as
formulas, proofs, and programs. Current implementations of
lambda Prolog, however, have no provision for a programmer to
provide a *concrete syntax* for a particular object-level
language. Such a capability is desirable, for example, in implementing
an interactive theorem prover. Providing the user with a familiar
syntax for the logic being implemented can greatly enhance
interaction. In this paper, we extend the Definite Clause Grammar
formalism of Prolog to a typed higher-order version in lambda Prolog
and show how such grammars can be applied to the problem of parsing
concrete syntax into higher-order syntax. We also present a program
for translating grammar specifications to lambda Prolog programs.
These programs serve as parsers for the specified languages. This
translation is itself presented as a lambda Prolog program.