Higher-Order Logic Programming: Summary of Lectures

Lecture 1 (May 4)

Topic
An informal introduction to lambda Prolog and its new programming language features: scoping mechanisms, higher-order programming, lambda terms as data structures.
References
  1. G. Nadathur and D. Miller, Higher-Order Logic Programming. To appear in Handbook of Logic in AI and Logic Programming, D. Gabbay, C. Hogger and A. Robinson (eds.) Only Section 2. (Main)
  2. G. Nadathur, B. Jayaraman and K. Kwon, Scoping Constructs in Logic Programming. To appear in Journal of Logic Programming. Only Section 2. (Main)
  3. D. Miller, Abstractions in Logic Programming. In Logic and Computer Science, P Odifreddi (ed.), Academic Press, pages 329 - 359, 1990.

Lecture 2 (May 11)

Topic
Introduction to a higher-order logic; simply typed lambda terms, lambda conversion, logical constants and formalization of their semantics via proof rules, comparison to first-order logic, predicate quantification, general and standard semantics.
References
  1. G. Nadathur and D. Miller, Higher-Order Logic Programming. To appear in Handbook of Logic in AI and Logic Programming, D. Gabbay, C. Hogger and A. Robinson (eds.). Only Section 3. (Main)
  2. Other references include [And71], [Chu40], [Hen50] in first reference.

Lecture 3 (May 18)

Topic
Uniform proofs as a foundation for logic programming, Horn clause logic as an abstract logic programming language, hereditary Harrop formulas.
References
  1. D. Miller, G. Nadathur, F. Pfenning and A. Scedrov, Uniform Proofs as a Foundation for Logic Programming, Annals of Pure and Applied Logic 51: 125 - 157, 1991. (Main)
  2. D. Loveland and G. Nadathur, Proof Procedures in Logic Programming. To appear in Handbook of Logic in AI and Logic Programming, D. Gabbay, C. Hogger and A. Robinson (eds.). Only Section 2. (Main)

Lecture 4 (June 1)

Topic
Higher-order hereditary Harrop formulas, development of a proof procedure, tagged higher-order unification.
References
  1. D. Miller, G. Nadathur, F. Pfenning and A. Scedrov, Uniform Proofs as a Foundation for Logic Programming, Annals of Pure and Applied Logic 51: 125 - 157, 1991. (Main)
  2. G. Nadathur, A Proof Procedure for the Logic of Hereditary Harrop Formulas, Journal of Automated Reasoning 11: 115-145, 1993. (Main)
  3. G. Nadathur and D. Miller, Higher-Order Logic Programming. To appear in Handbook of Logic in AI and Logic Programming, D. Gabbay, C. Hogger and A. Robinson (eds.) Only Section 6. (Main)
  4. G. Huet, A Unification Algorithm for Typed lambda-Calculus, Theoretical Computer Science 1:27-57, 1973. (Main)
  5. C. Elliott and F. Pfenning, A Semi-Functional Implementation of a Higher-Order Logic Programming Language. In Topics in Advanced Language Implementation, P. Lee (ed.), MIT Press, 1991, pages 289 - 325.
  6. W. Snyder and J. Gallier, Higher-Order Unification Revisited: Complete Sets of Transformations, Journal of Symbolic Computation 8: 101 - 140, 1989.
  7. D. Miller, Unification under a Mixed Prefix, Journal of Symbolic Computation 14: 321 - 358, 1992.
  8. W. Goldfarb, The Undecidability of the Second-Order Unification Problem, Theoretical Computer Science 13:225-230, 1981. (Aux)
  9. G. Huet, The Undecidability of Unification in Third Order Logic, Information and Control 22:257 - 267, 1973. (Aux)
  10. G. Huet and B. Lang, Proving and Applying Program Transformations Expressed with Second-Order Patterns, Acta Informatica 11: 31 - 55, 1978. (Aux)
  11. G. Dowek, Third-Order Matching is Decidable, Annals of Pure and Applied Logic 69: 135 - 155, 1994. (Aux)

Lecture 5 (June 8)

Topic
Continuation of discussions of Lecture 4.
References
Same as for Lecture 4

Lecture 6 (June 22)

Topic
Lambda Prolog as a programming language based on higher-order hereditary Harrop formulas. Applications of lambda Prolog in higher-order programming and meta-programming. Higher-order abstract syntax.
References
  1. G. Nadathur and D. Miller, Higher-Order Logic Programming. To appear in Handbook of Logic in AI and Logic Programming, D. Gabbay, C. Hogger and A. Robinson (eds.) Sections 7, 8 and 9 will be covered in Lectures 6, 7 and 8. (Main)
  2. D. Miller and G. Nadathur, A Logic Programming Approach to Manipulating Formulas and Programs. In Proceedings of the IEEE Symposium on Logic Programming, September 1987, pages 379 - 388. (Main)
  3. F. Pfenning and C. Elliott, Higher-Order Abstract Syntax. In Proceedings of the ACM SIGPLAN '88 Symposium on Language Design and Implementation, June 1988, pages 199 - 208.
  4. A. Felty and D. Miller, Specifying Theorem Provers in a Higher-Order Logic Programming Language. In Proceedings of the Ninth International Conference on Automated Deduction, E. Lusk and R. Overbeek (eds.), May 1988, Springer-Verlag LNCS 310, pages 61 - 80.
  5. D. Miller and G. Nadathur, Some Uses of Higher-Order Logic in Computational Linguistics. In Proceedings of the 24th Annual Meeting of the Association for Computational Linguistics, June 1986, 247 -- 255. (Aux)
  6. A. Felty, Specifying and Implementing Theorem Provers in a Higher-Order Logic Programming Language, Ph.D. Thesis, University of Pennsylvania, August 1989. Available as UPenn Tech Report MS-CIS-89-53. (Aux)
  7. J. J. Hannan, Investigating a Proof-Theoretic Meta-Language for Functional Programs, Ph.D Thesis, University of Pennsylvania, January 1991. Available as UPenn Technical Report MS-CIS-91-09. (Aux)
  8. R. Pareschi, Type-Driven Natural Language Analysis, Ph.D. Thesis, University of Edinburgh, 1989. (Aux)
  9. S. Dietzen, A language for Higher-Order Explanation Based Learning, Ph.D. Thesis, School of Computer Science, Carnegie Mellon University, 1991. Available as CMU Technical Report CMU-CS-92-110. (Aux)

Lecture 7 (July 6)

Topic
Introduction to the lambda Prolog system, metalanguage applications. (This lecture will be held in a room equipped with a computer, room to be announced in class.)
References
  1. Handout to be given in a previous lecture.
  2. A. Felty and D. Miller, Specifying Theorem Provers in a Higher-Order Logic Programming Language. In Proceedings of the Ninth International Conference on Automated Deduction, E. Lusk and R. Overbeek (eds.), May 1988, Springer-Verlag LNCS 310, pages 61 - 80. (Main)
  3. A description of the system that we will install at LMU may be available later in this space.

Lecture 8 (July 13)

Topic
Further discussions of metalanguage aspects, the sublanguage L_lambda and its applications.
References
  1. G. Nadathur and D. Miller, Higher-Order Logic Programming. To appear in Handbook of Logic in AI and Logic Programming, D. Gabbay, C. Hogger and A. Robinson (eds.) Focus on Sections 8 and 9. (Main)
  2. D. Miller, A Logic Programming Language with lambda-Abstraction, Function Variables, and Simple Unification, Journal of Logic and Computation 1(4): 497 - 536, 1991. (Main)
  3. T. Nipkow, Functional Unification of Higher-Order Patterns. In Proceedings of the Eighth Annual {IEEE} Symposium on Logic in Computer Science, M. Vardi (ed), 1993.

Lecture 9 (July 20)

Topic
Implementation issues related to lambda Prolog, clause scoping and backtracking, lambda term representation, higher-order unification and branching.
References
  1. G. Nadathur, B. Jayaraman and K. Kwon, Scoping Constructs in Logic Programming. To appear in Journal of Logic Programming.
  2. G. Nadathur, B. Jayaraman and D. S. Wilson, Implemention Considerations for Higher-Order Features in Logic Programming, Duke Technical Report CS-1993-16.
  3. K. Kwon and G. Nadathur, An Instruction Set for Higher-Order Hereditary Harrop Formulas (Extended Abstract), Proceedings of the Workshop on the lambda Prolog Programming Language, Philadelphia, 1992. Proceedings available as UPenn Technical Report MS-CIS-92-86.
  4. G. Nadathur and D.S. Wilson, A Notation for Lambda Terms I: A Generalization of Environments, Duke Technical Report CS-1994-03. (Aux)
  5. G. Nadathur, A Notation for Lambda Terms II: Refinements and Applications, Duke Technical Report CS-1994-01. (Aux)
  6. P. Brisset and O. Ridoux, Naive Reverse can be Linear. In Proceedings of the Eighth International Conference on Logic Programming, MIT Press, 1991, pages 857 - 870. (Aux)
  7. P. Brisset and O. Ridoux, The Compilation of lambda Prolog and its execution with MALI. Publication Interne No 687, IRISA, Rennes, November, 1992.
  8. M. Abadi, L. Cardelli, P.-L. Curien and J.-J. Levy, Explicit Substitutions. In Proceedings of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, ACM Press, pages 31 - 46, January, 1990. (Aux)
  9. G. Dowek, T. Hardin and C. Kirchner, Higher-Order Unification via Explicit Substitutions. (Instructor has shorter version that is to appear in Proceedings of the Tenth Annual Symposium on Logic in Computer Science, D. Kozen (ed.), IEEE Computer Society Press, June 1995.) (Aux)

Last updated on April 27, 1995 by gopalan@takapoto.pms.informatik.uni-muenchen.de