Kripke semantics for higher-order type theory applied to constraint logic programming languages

We define a Kripke semantics for Intuitionistic Higher-Order Logic with constraints formulated within Church's Theory of Types via the addition of a new constraint base type. We then define an executable fragment, hoHH(C), of the logic: a higher-order logic programming language with typed lambda-abstraction, implication and universal quantification in goals and constraints, and give a modified model theory for this fragment. Both formal systems are shown sound and complete for their respective semantics. We also solve the impredicativity problem in lambda Prolog semantics, namely how to give a definition of truth without appealing to induction on subformula structure. In the last section we give a simple semantics-based conservative extension proof that the language hoHH(C) satisfies a uniformity property along the lines of [39]. (C) 2017 Elsevier B.V. All rights reserved.