ûProlog, also written lambda Prolog, is a logic programming language featuring polymorphic typing, modular programming, and higher-order programming. 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.
Since 1986, ûProlog has received numerous implementations. As of 2023, the language and its implementations are still actively being developed.
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. Implication is used for local scoping of predicate definitions while universal quantification is used for local scoping of variables, as in the following implementation of reverse depending on an auxiliary rev predicate:
A common use of these scoping constructs is to simulate scope often seen in an inference-rule presentation of a logic. For example, proof search (and proof checking) in natural deduction may be encoded as follows: