|
Título:
|
Higher-order logic programming languages with constraints: A semantics
|
|
Autores:
|
Nieva Soto, Susana ;
Lipton, James
|
|
Tipo de documento:
|
texto impreso
|
|
Editorial:
|
Springer Verlag Berlín, 2007
|
|
Dimensiones:
|
application/pdf
|
|
Nota general:
|
info:eu-repo/semantics/restrictedAccess
|
|
Idiomas:
|
|
|
Palabras clave:
|
Estado = Publicado
,
Materia = Ciencias: Informática: Lenguajes de programación
,
Tipo = Sección de libro
|
|
Resumen:
|
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 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).
|
|
En línea:
|
https://eprints.ucm.es/id/eprint/17160/1/Nieva03.pdf
|
