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

terminationsubstitutionsCambridge LCF theorem prover

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

(11)

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

Describes a project that uses

Uses Software

• LCF
• HOL

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)