Verifying the unification algorithm in LCF

DOI10.1016/0167-6423(85)90009-7MaRDI QIDQ1060023zbMATH OpenOpenAlexWikidataFDO

Authors Lawrence C. Paulson

Publication date 1985

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0167-6423(85)90009-7

zbMATH Keywords

Cambridge LCF theorem proversubstitutionstermination

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Lessons learned from LCF: A Survey of Natural Deduction Proofs
• Verification of the Completeness of Unification Algorithms à la Robinson
• First-order unification by structural recursion
• scientific article; zbMATH DE number 3858458
• Formal correctness of a quadratic unification algorithm

Cited in

(12)

• A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
• Formalization of the resolution calculus for first-order logic
• Completeness in PVS of a nominal unification algorithm
• Unification: A case-study in data refinement
• Unification via the s_e-style of explicit substitutions
• First-order unification by structural recursion
• Lessons learned from LCF: A Survey of Natural Deduction Proofs
• Verification of the Completeness of Unification Algorithms à la Robinson
• A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
• A certified implementation of ML with structural polymorphism and recursive types
• Automating the derivation of unification algorithms. A case study in deductive program synthesis
• Partial and nested recursive function definitions in higher-order logic

Describes a project that uses

Uses Software

• HOL
• LCF

This page was built for publication: Verifying the unification algorithm in LCF

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1060023)