Term Rewriting and All That
ML programs, by chapter
Appendix 2
: a library of basic ML functions.
Chapter 2
: lexicographic and multiset orders.
Chapter 4
: terms, unification, matching, normalization.
Chapter 5
: term orders.
Chapter 6
: Critical Pairs.
Chapter 7
: Knuth-Bendix completion à la Huet.
Chapter 9
: combination of decision procedures for word problems.
Chapter 10
: Boolean unification.
A textbook:
ML for the Working Programmer
General information on ML