Unification is a major technique in implementing and understanding programming languages.
We use it for pattern matching, semantics, higher order type checking, and there is even
an entire programming language that uses unification to drive computation.
Videos