Sun 22 - Fri 27 October 2023 Cascais, Portugal
Mon 23 Oct 2023 11:10 - 12:10 at Room VII - Session I Chair(s): Santiago Escobar, Robert Glück

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

11:00 - 12:30
Session ILOPSTR at Room VII
Chair(s): Santiago Escobar , Robert Glück University of Copenhagen
Day opening
Opening Remarks
Robert Glück University of Copenhagen
Unification Modulo Equational Theories in Languages with Binding Operators Keynote
Maribel Fernandez King's College London
Towards a Certified Proof Checker for Deep Neural Network Verification
Remi Desmartin Heriot-Watt University, Omri Isac The Hebrew University of Jerusalem, Grant Passmore Imandra Inc., Kathrin Stark Heriot-Watt University, Guy Katz Hebrew University, Ekaterina Komandantskaya Heriot-Watt University, UK

Information for Participants
Info for event:

Together with PPDP