Aviso: Por labores de mantenimiento y mejora del repositorio, el martes día 1 de Julio, Docta Complutense no estará operativo entre las 9 y las 14 horas. Disculpen las molestias.
 

Higher-order logic programming languages with constraints: A semantics

Loading...
Thumbnail Image

Full text at PDC

Publication date

2007

Advisors (or tutors)

Journal Title

Journal ISSN

Volume Title

Publisher

Springer Verlag Berlín
Citations
Google Scholar

Citation

Abstract

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).

Research Projects

Organizational Units

Journal Issue

Description

8th International Conference,TLCA 2007, Paris, France,June 26-28, 2007. Proceedings

Keywords