Hashing Modulo Context-Sensitive Alpha-Equivalence - PLDI 2024

Explore a video presentation from the PLDI 2024 conference that delves into the concept of hashing modulo context-sensitive alpha-equivalence in lambda calculus. Learn about the limitations of traditional alpha-equivalence when comparing subterms within larger contexts and discover a new formal notion of context-sensitive alpha-equivalence. Understand how this equivalence relates to bisimulation equivalence and examine an efficient O(n log n) runtime hashing scheme for identifying lambda-terms modulo context-sensitive alpha-equivalence. Gain insights into the practical applications of this hashing technique, including common subterm elimination and structure sharing. See how the presented algorithm has been applied to create a densely packed, interconnected graph of mathematical knowledge from the Coq proof assistant for machine learning purposes.