Linear unification of higher-order patterns

DOI10.1007/3-540-56610-4_78zbMath1497.68096OpenAlexW1577812319MaRDI QIDQ5044750

Zhenyu Qian

Publication date: 2 November 2022

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-56610-4_78

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Combinatory logic and lambda calculus (03B40)

Related Items (7)

Higher-order rewrite systems and their confluence ⋮ Unnamed Item ⋮ Constraint handling rules with binders, patterns and generic quantification ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Inductive-data-type systems ⋮ Unification with extended patterns ⋮ The practice of logical frameworks

Uses Software

• Elf

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The undecidability of the second-order unification problem
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Linear unification
• An Efficient Unification Algorithm
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification

This page was built for publication: Linear unification of higher-order patterns