SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Mon 23 Oct 2023 11:10 - 12:10 at Room VII - Session 6 Chair(s): Santiago Escobar

Unification (i.e., solving equations between terms) is a key step in the implementation of logic programming languages and theorem provers, and is also used in type inference algorithms for functional languages and as a mechanism to analyse rewrite-based specifications (e.g., to find critical pairs). Matching is a version of unification in which only one of the terms in the equation can be instantiated. Often, operators satisfy equational axioms (e.g., associativity, commutativity), which must be taken into account during the unification or matching process. In addition, when the expressions to be unified involve binding operators (as is the case when representing programs, logics, computation models, etc.), unification and matching algorithms must take into account the alpha-equivalence relation generated by the binders. In this talk, we present matching and unification algorithms for languages that include binding operators as well as operators that satisfy equational axioms, such as associativity and commutativity.

Mon 23 Oct

Displayed time zone: Lisbon change