Unification
Union Find
Higher Order Unification
efficient full higher order unification zipperposition
Pattern Matching
Arguably pattern matching should be it’s own article. Depending on which you see first, you may consider unification two way pattern matching or pattern matching as one way unification. I think pattern matching is the much simpler topic
Resources
higher order pattern unification exampel in elaboration zoo Basic pattern unification in haskell
What is the pattern fragment? L_lambda subset “existential variables” applied to unique bound variables. reminscent of haskell pattern matching using distinct variables
http://conal.net/papers/elliott90.pdf conal elliott’s thesis
https://conservancy.umn.edu/bitstream/handle/11299/57268/Qi_umn_0130E_10758.pdf?sequence=1 lambda prolog implementation
See Miller and Nadathur book.
Tiark Rompf nbe?