Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type
From MaRDI portal
Publication:5055872
DOI10.1007/3-540-61464-8_64zbMATH Open1503.68108OpenAlexW1544708439MaRDI QIDQ5055872FDOQ5055872
Authors: Roland Fettig, Bernd Löchner 
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
Recommendations
Cites Work
- Title not available (Why is that?)
- A unification algorithm for typed \(\overline\lambda\)-calculus
- The undecidability of the second-order unification problem
- Higher-order unification revisited: Complete sets of transformations
- Title not available (Why is that?)
- A confluent reduction for the extensional typed \(\lambda\)-calculus with pairs, sums, recursion and terminal object
- The virtues of eta-expansion
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
- Unification with extended patterns
- Title not available (Why is that?)
Cited In (9)
- Functions-as-constructors higher-order unification: extended pattern unification
- Title not available (Why is that?)
- Higher-order dynamic pattern unification for dependent types and records
- Higher-order pattern complement and the strict \(\lambda\)-calculus
- Optimizing higher-order pattern unification.
- Higher-order unification via combinators
- Two thoughts on higher-order unification -- most relevant unifiers and unification with case distinction
- Logic Programming
- Title not available (Why is that?)
This page was built for publication: Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5055872)
