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)

• Verifying the unification algorithm in LCF
• Restricted combinatory unification
• Executable relational specifications of polymorphic type systems using Prolog
• Auto in Agda. Programming proof search using reflection
• A unified treatment of syntax with binders
• Everybody's got to be somewhere
• First-order unification in the PVS proof assistant
• A library for polymorphic dynamic typing
• Partiality and recursion in interactive theorem provers -- an overview
• (Nominal) unification by recursive descent with triangular substitutions

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)