These extensions to Prolog are derived from the higher-order hereditary Harrop formulas used to justify the foundations of λProlog.
Higher-order quantification, simply typed λ-terms, and higher-order unification gives λProlog the basic supports needed to capture the λ-tree syntax approach to higher-order abstract syntax, an approach to representing syntax that maps object-level bindings to programming language bindings.
Programmers in λProlog need not deal with bound variable names: instead various declarative devices are available to deal with binder scopes and their instantiations.
The Abella theorem prover has been designed to provide an interactive environment for proving theorems about the declarative core of λProlog.
Two unique features of λProlog include implications and universal quantification.