Beta Unification is a generalization of first-order unification which was
introduced in the last two years to characterize typability of lambda-terms in
the system of intersection types (in just the same way in which first-order
unification can be used to characterize typability of lambda-terms in the system
of simple types). The system of intersection types enjoys strong normalization,
subject reduction and, under a finite-rank restriction, computable type
inference, just as it supports a pragmatics for implementing parametric
polymorphism. In this talk, we review the fundamentals of beta unification,
explain the connection with intersection types, and motivate its use in the
analysis of programs.