First-order unification by structural recursion

DOI10.1017/S0956796803004957MaRDI QIDQ3160301zbMATH OpenOpenAlexWikidataFDO

Authors Conor McBride

Publication date 8 February 2005

Published in Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0956796803004957

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• (Nominal) unification by recursive descent with triangular substitutions
• First-order unification in the PVS proof assistant
• Verifying the unification algorithm in LCF
• scientific article; zbMATH DE number 3858458
• Verification of the Completeness of Unification Algorithms à la Robinson

Cited in

(10)

• scientific article; zbMATH DE number 7447767 (Why is no real title available?)
• Restricted combinatory unification
• Verifying the unification algorithm in LCF
• Auto in Agda. Programming proof search using reflection
• Executable relational specifications of polymorphic type systems using Prolog
• (Nominal) unification by recursive descent with triangular substitutions
• Partiality and recursion in interactive theorem provers -- an overview
• A unified treatment of syntax with binders
• First-order unification in the PVS proof assistant
• A library for polymorphic dynamic typing

This page was built for publication: First-order unification by structural recursion

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