An Explicit Substitution Notation in a lambda Prolog Implementation
Gopalan Nadathur · 1998
This extended abstract has a pragmatic intent: it explains the use of an explicit substitution notation in an implementation of the higher-order logic programming language lambda Prolog. In particular, it describes an explicit substitution calculus for lambda terms that is called the annotated suspension notation, then presents a stack based procedure for head-normalizing terms in this notation and, finally, explains how these various aspects fit into an implementation of higher-order unification. All the devices sketched in this paper have been used in a C-based implementation of an abstract machine for lambdaProlog.