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.