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

Jozef g explanation

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?