Verifying the unification algorithm in LCF

This publication has 13 references indexed in Scilit:

• Constructive Mathematics and Computer Programming
  Published by Elsevier ,2014
• A theory of type polymorphism in programming
  Published by Elsevier ,2003
• Synthesis of a unification algorithm in a logic programming calculus
  The Journal of Logic Programming, 1984
• A Mechanical Proof of the Turing Completeness of Pure Lisp
  Contemporary Mathematics, 1984
• The Equivalence of Two Semantic Definitions: A Case Study in LCF
  SIAM Journal on Computing, 1983
• Deductive synthesis of the unification algorithm
  Science of Computer Programming, 1981
• Edinburgh LCF
  Lecture Notes in Computer Science, 1979
• A Computational Logic
  Published by Elsevier ,1979
• Proving Properties of Programs by Structural Induction
  The Computer Journal, 1969
• On the recursive programming techniques
  Communications of the ACM, 1964