title: Higher-order unification
body: <p>I'm working on a higher-order theorem prover, of which unification seems to be the most difficult subproblem.</p>
  
  <p>If Huet's algorithm is still considered state-of-the-art, does anyone have any links to explanations of it that are written to be understood by a programmer rather than a mathematician?</p>
  
  <p>Or even any examples of where it works and the usual first-order algorithm doesn't?</p>