Welcome to Higher Order Prolog with Extensional Semantics

Hopes is a prototype interpreter for the definitorial higher order PROLOG. The interpreter implements a higher order proof procedure with extensional semantics.