Publication: Higher-order logic programming languages with constraints: A semantics
Loading...
Full text at PDC
Publication Date
2007
Authors
Advisors (or tutors)
Editors
Journal Title
Journal ISSN
Volume Title
Publisher
Springer Verlag Berlín
Citations
Exportar
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).
Description
8th International Conference,TLCA 2007, Paris, France,June 26-28, 2007. Proceedings
UCM subjects
Unesco subjects
Keywords
Citation
Andrews, P.: Resolution in type theory. Journal of Symbolic Logic, 36(3) (1971)
Bai, M., Blair, H.: General model theoretic semantics for higher-order horn logic programming. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, Springer, Heidelberg (1992)
Benzmüller, C., Brown, C.E., Kohlhase, M.: Higher order semantics and extensionality. Journal of Symbolic Logic 69, 1027–1088 (2004)
Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic 5, 56–68 (1940)
DeMarco, M.: Higher Order Logic Programming in the Theory of Types. PhD thesis, Wesleyan University (1999)
DeMarco, M., Lipton, J.: Completeness and cut elimination in the intuitionistic theory of types. The Journal of Logic and Computation 15(6), 821–854 (2005)
Gabbay, D.M., Reyle, U.: N-prolog: an extension of prolog with hypothetical implications i. Journal of Logic Programming 1(4), 319–355 (1984)
García-Díaz, M., Nieva, S.: Providing declarative semantics for HH extended constraint logic programs. In: PPDP ’04, pp. 55–66. ACM Press, New York (2004)
Girard, J., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge University Press, Cambridge (1998)
Henkin, L.: Completeness in the theory of types. Journal of Symbolic Logic 15, 81–91 (1950)
Hindley, J.R.: Basic simple type theory. Cambridge University Press, Cambridge (1997)
Jaffar, J., Maher, M.: Constraint logic programming: A survey. Journal of Logic Programming 19/20, 503–581 (1994)
Jagadeesan, R., Nadathur, G., Saraswat, V.A.: Testing concurrent systems: An interpretation of intuitionistic logic. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 517–528. Springer, Heidelberg (2005)
Lastres, E.: A Semantics for Logic Programs based on HH Formulas. PhD thesis, Università di Pisa (2002)
Leach, J., Nieva, S.: A higher-order logic programming language with constraints. In: Kuchen, H., Ueda, K. (eds.) FLOPS 2001. LNCS, vol. 2024, pp. 108–122. Springer, Heidelberg (2001)
Leach, J., Nieva, S., Rodríguez-Artalejo, M.: Constraint logic programming with hereditary Harrop formulas. Theory and Practice of Logic Programming 1(4), 409–445 (2001) » CrossRef
Miller, D.: A logical analysis of modules in logic programming. Journal of Logic Programming, 79–108 (1989)
Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic 51(1-2), 125–157 (1991)
Mitchell, J.: Foundations for Programming Languages. MIT Press, Cambridge, MA (1996)
Mitchell, J., Moggi, E.: Kripke-style models for typed lambda calculus. Annals of Pure and Applied Logic 51, 99–124 (1991)
Nadathur, G.: A proof procedure for the logic of hereditary harrop formulas. Journal of Automated Reasoning 11, 115–145 (1993)
Saraswat, V.: The category of constraints is cartesian closed. In: LICS ’92. Proc. of the 7th Symposium on Logic in Computer Science, pp. 341–345. IEEE Computer Society Press, Los Alamitos (1992)
Takahashi, M.: A proof of cut-elimination in simple type theory. J. Math. Soc. Japan 19(4), 399–410 (1967)
Tarski, A.: A decision method for elementary algebra and geometry. University of California Press, Berkeley (1951)
van Dalen, D.: Logic and Structure. Springer, Heidelberg (2004)
Wolfram, D.A.: A semantics for λprolog. Theoretical Computer Science 136, 277–289 (1994)