A logic programming approach to implementing higher-Order term rewriting

This publication has 16 references indexed in Scilit:

• Specifying theorem provers in a higher-order logic programming language
  Published by Springer Nature ,2005
• A computation model for executable higher-order algebraic specification languages
  Published by Institute of Electrical and Electronics Engineers (IEEE) ,2002
• Encoding dependent types in an intuitionistic logic
  Published by Cambridge University Press (CUP) ,1991
• Polymorphic rewriting conserves algebraic strong normalization
  Theoretical Computer Science, 1991
• Uniform proofs as a foundation for logic programming
  Annals of Pure and Applied Logic, 1991
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
  Journal of Logic and Computation, 1991
• Equational reasoning in Isabelle
  Science of Computer Programming, 1989
• Edinburgh LCF
  Lecture Notes in Computer Science, 1979
• A unification algorithm for typed λ-calculus
  Theoretical Computer Science, 1975
• A formulation of the simple theory of types
  The Journal of Symbolic Logic, 1940