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

We also solve the impredicativity problem in λ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].