In this talk I will present joint work with Beniamino Accattoli and Claudio Sacerdoti Coen, accepted at PPDP 19. The topic is how to check efficiently whether given -terms are equal, or more precisely -equal: as simple as it may sound, the problem is non-trivial when -terms are represented succintly with sharing, i.e. the reuse of subterms. This problem is relevant in implementations of the -calculus, for instance in proof assistants: type-checking algorithms for dependent type theories rely on a conversion subprocedure to check whether two -terms are convertible, i.e. they reduce to the same term. A lot of research has been carried on how to evaluate -terms in an efficient way, which boils down to use sharing in one way or another; the missing part is how to compare the shared results for equality.

In presence of sharing, one is actually interested in sharing equality, i.e. the equality of the underlying unshared -terms. The naive algorithm for sharing equality is exponential in the size of the shared terms, but in this talk I will present our linear-time algorithm (the first with such low complexity). As others before us, we were inspired by Paterson and Wegman's algorithm for first-order unification, itself based on representing terms with sharing as DAGs, and sharing equality as bisimulation of DAGs.