Sciweavers

Share
TLCA
2007
Springer

Higher-Order Logic Programming Languages with Constraints: A Semantics

10 years 4 months ago
Higher-Order Logic Programming Languages with Constraints: A Semantics
A 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 λ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 lambdaion, implication and universal quantification in goals and constraints. This provides a Kripke semantics for the full higher-order hereditarily Harrop logic of λProlog as a special case (with the constraint system chosen to be β,η-conversion).
James Lipton, Susana Nieva
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where TLCA
Authors James Lipton, Susana Nieva
Comments (0)
books