Uniform Algebras: Models and constructive Completeness for Full, Simply Typed λProlog

Gianluca Amato, Mary DeMarco, James Lipton

This paper introduces a model theory for resolution on Higher Order Hereditarily Harrop formulae (HOHH), the logic underlying the Lambda-Prolog programming language, and proves sou…