Verifying the unification algorithm in LCF

DOI10.1016/0167-6423(85)90009-7zbMath0567.68054OpenAlexW2019994514WikidataQ57382754 ScholiaQ57382754MaRDI QIDQ1060023

Lawrence Charles 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)

Related Items (7)

Unification: A case-study in data refinement ⋮ Formalization of the resolution calculus for first-order logic ⋮ A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading ⋮ Completeness in PVS of a nominal unification algorithm ⋮ A certified implementation of ML with structural polymorphism and recursive types ⋮ Partial and nested recursive function definitions in higher-order logic ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction

Uses Software

• HOL
• LCF

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