Unification Modulo Equational Theories in Languages with Binding Operators

Explore unification and matching algorithms for languages with binding operators and equational axioms in this 59-minute conference talk presented by Maribel Fernandez at LOPSTR23. Delve into the complexities of solving equations between terms, a crucial process in logic programming languages, theorem provers, and type inference algorithms for functional languages. Examine how equational axioms like associativity and commutativity affect the unification and matching processes, and learn about the challenges posed by alpha-equivalence in expressions with binding operators. Gain insights into advanced algorithms designed to handle these complex scenarios, essential for analyzing rewrite-based specifications and implementing sophisticated programming language features.