  The notion of $\alpha$-equivalence between $\lambda$-terms is commonly used
to identify terms that are considered equal. However, due to the primitive
treatment of free variables, this notion falls short when comparing subterms
occurring within a larger context. Depending on the usage of the Barendregt
convention (choosing different variable names for all involved binders), it
will equate either too few or too many subterms. We introduce a formal notion
of context-sensitive $\alpha$-equivalence, where two open terms can be compared
within a context that resolves their free variables. We show that this
equivalence coincides exactly with the notion of bisimulation equivalence.
Furthermore, we present an efficient $O(n\log n)$ runtime hashing scheme that
identifies $\lambda$-terms modulo context-sensitive $\alpha$-equivalence,
generalizing over traditional bisimulation partitioning algorithms and
improving upon a previously established $O(n\log^2 n)$ bound for a hashing
modulo ordinary $\alpha$-equivalence by Maziarz et al. Hashing $\lambda$-terms
is useful in many applications that require common subterm elimination and
structure sharing. We have employed the algorithm to obtain a large-scale,
densely packed, interconnected graph of mathematical knowledge from the Coq
proof assistant for machine learning purposes.
