Version 5 (modified by acharal, 5 years ago)


Welcome to Higher Order Prolog with Extensional Semantics

HOPES is a prototype interpreter written in Haskell for the definitorial higher order PROLOG. The interpreter implements a higher order proof procedure with extensional semantics.

For more information about the formal definition of the language and its semantics you should consult this paper.

Getting Started with the Interpreter

To checkout the source from the darcs repository you should execute

darcs get hopes

To compile the source you must install the cabal package and execute



  • Can write first-order programs like ordinary Prolog.
  • Higher-Order Variables: Can be passed as arguments and called like ordinary predicates.
  • Partial Applications: Predicates can be applied only to some of their arguments.
  • Lambda Abstractions: Support of anonymous predicate definition using lambda abstractions.
  • Existential Higher-Order Variables: Can query a variable relation and generate an appropriate extensional binding.


In order to gain some intuition behind logic programming in HOPES some simple examples are given.

The ordered predicate is the simple second-order predicate that holds if the relation R is an ordering of the list.

ordered(R, []).
ordered(R, [X]).
ordered(R, [X, Y| Z]):- R(X,Y), ordered(R, [Y|Z]).

The popular map predicate:

map(R, [], []).
map(R, [X|Xs], [Y|Ys]) :- R(X, Y), map(R, Xs, Ys).

Other Higher Order Logic Systems