Nieva Soto, SusanaLipton, JamesRonchi della Rocca, Simona2023-06-202023-06-202007978-3-540-73227-310.1007/978-3-540-73228-0 20https://hdl.handle.net/20.500.14352/531728th International Conference,TLCA 2007, Paris, France,June 26-28, 2007. ProceedingsA Kripke Semantics is defined for a higher-order logic programming language with constraints, based on Church's Theory of Types and a generic constraint formalism. Our syntactic formal system, hoHH(C) (higher-order hereditary Harrop formulas with constraints), which extends lambda Prolog's logic, is shown sound and complete. A Kripke semantics for equational reasoning in the simply typed lambda-calculus (Kripke Lambda Models) was introduced by Mitchell and Moggi in 1990. Our model theory extends this semantics to include full impredicative higher-order intuitionistic logic, as well as the executable hoHH fragment with typed lambda-abstraction, implication and universal quantification in goals and constraints. This provides a Kripke semantics for the full higher-order hereditarily Harrop logic of lambda Prolog as a special case (with the constraint system chosen to be,13,beta,eta-conversion).engbook parthttp://link.springer.com/chapter/10.1007%2F978-3-540-73228-0_20http://link.springer.com/restricted access004.43Lenguajes de programación1203.23 Lenguajes de Programación