Hashing Modulo Context-Sensitive Alpha-Equivalence - PLDI 2024
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
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.
Syllabus
[PLDI24] Hashing Modulo Context-Sensitive Alpha-Equivalence
Taught by
ACM SIGPLAN
Related Courses
Verifying the LLVMStrange Loop Conference via YouTube Beweisbar sichere Software
media.ccc.de via YouTube RustBelt: A Quick Dive Into the Abyss - Formalizing Rust's Safety Story
Rust via YouTube Building Measure Theory Using Hierarchy Builder
Hausdorff Center for Mathematics via YouTube Using Formal Methods to Eliminate Exploitable Bugs - YOW! 2015
GOTO Conferences via YouTube