Higher-order unification, polymorphism, and subsorts

DOI10.1007/3-540-54317-1_112OpenAlexW1152827136MaRDI QIDQ5881304

Tobias Nipkow

Publication date: 9 March 2023

Published in: Conditional and Typed Rewriting Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-54317-1_112

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Related Items

A restricted form of higher-order rewriting applied to an HDL semantics ⋮ A recursive path ordering for higher-order terms in η-long β-normal form ⋮ Introduction to ``Milestones in interactive theorem proving ⋮ Modularity of termination and confluence in combinations of rewrite systems with λω ⋮ Complete axiomatizations of some quotient term algebras ⋮ From LCF to Isabelle/HOL ⋮ Higher-order matching for program transformation ⋮ Completion of rewrite systems with membership constraints

Uses Software

• Haskell

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Order-sorted unification
• The undecidability of the second-order unification problem
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Computational aspects of an order-sorted logic with term declarations
• Higher-order unification revisited: Complete sets of transformations
• Natural deduction as higher-order resolution
• Higher-order unification with dependent function types