Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type

DOI10.1007/3-540-61464-8_64zbMath1503.68108OpenAlexW1544708439MaRDI QIDQ5055872

Bernd Löchner, Roland Fettig

Publication date: 9 December 2022

Published in: Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61464-8_64

Mathematics Subject Classification ID

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

Related Items (1)

Functions-as-constructors higher-order unification: extended pattern unification

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The undecidability of the second-order unification problem
• The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Unification with extended patterns
• Higher-order unification revisited: Complete sets of transformations
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object
• The virtues of eta-expansion

This page was built for publication: Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type