Summary: Stimulated by concerns of software certification especially as it relates to mobile code, formal structures such as specifications and proofs are beginning to play an explicit role in computing. In representing and manipulating such structures, an approach is needed that pays attention to the binding operation that is present in them. The language \(\lambda\)Prolog provides programming support for a higher-order treatment of abstract syntax that is especially suited to this task. This support is realized by enhancing the traditional strength of logic programming in the metalanguage realm with an ability for dealing directly with binding structure. This paper identifies the features of \(\lambda\)Prolog that endow it with such a capability, illustrates their use and and describes methods for their implementation. Also discussed is a new realization of \(\lambda\)Prolog called Teyjus that incorporates the implementation ideas presented.
For the entire collection see [Zbl 0958.00038].