Functions-as-constructors Higher-order Unification

DOI10.4230/LIPIcs.FSCD.2016.26zbMath1387.03008OpenAlexW2484664235MaRDI QIDQ5369491

Tomer Libal, Dale A. Miller

Publication date: 17 October 2017

Full work available at URL: https://hal.inria.fr/hal-01379683

zbMATH Keywords

higher-order unificationpattern unification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Related Items

Functions-as-constructors higher-order unification: extended pattern unification ⋮ Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding ⋮ Unnamed Item ⋮ How to prove decidability of equational theories with second-order computation analyser SOL ⋮ Unnamed Item ⋮ Restricted combinatory unification ⋮ A Generic Framework for Higher-Order Generalizations. ⋮ Implementing type theory in higher order constraint logic programming

Uses Software

• Beluga
• Isabelle/HOL
• THF0
• Satallax
• Twelf
• Abella
• Agda
• Minlog
• Leo-III
• Leo
• Teyjus

This page was built for publication: Functions-as-constructors Higher-order Unification