Nieva Soto, SusanaLipton, JamesRonchi della Rocca, Simona2023-06-202023-06-202007Andrews, 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)978-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