3 | | HOPES is a prototype interpreter written in [http://www.haskell.org/haskellwiki/Haskell Haskell] for the definitorial higher order [http://en.wikipedia.org/wiki/Prolog PROLOG]. |

4 | | The interpreter implements a higher order proof procedure with extensional semantics. |

| 3 | Hopes is a prototype interpreter for a higher-order PROLOG-like |

| 4 | language. The syntax of the language extends that of [http://en.wikipedia.org/wiki/Prolog PROLOG] by |

| 5 | supporting higher-order constructs (such as higher-order predicate |

| 6 | variables, partial application and lambda terms). In particular, |

| 7 | the syntax allows clauses (and queries) that contain uninstantiated |

| 8 | predicate variables. The interpreter implements a higher-order |

| 9 | top-down SLD-resolution proof procedure described in [http://arxiv.org/abs/1106.3457 this paper]. In the |

| 10 | case of uninstantiated predicate variables, the proof procedure |

| 11 | will systematically (and in a sophisticated way) investigate all |

| 12 | finite instantiations of these variables. |