Unification Modulo Equational Theories in Languages with Binding Operators
summary
Presents concrete algorithms and implementations for solving equations where terms have binders plus equational axioms: uses nominal logic with permutations to encode alpha-equivalence, yields nominal unification is decidable and unitary, and gives matching algorithms that run as fast as first-order for ground terms. Worst-case unification is quadratic (matching linear; equivariant matching exponential), AC cases require fixpoint constraints to stay finitary, and full implementations and proofs appear in Coq and PVS plus AlphaProlog/Isabelle libraries.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:48Talk overview
- 3:36Languages with binders
- 6:28Binders: intuitive and formal
- 13:32Nominal logic basics
- 18:14Nominal syntax and unification
- 25:24Alpha equivalence and freshness
- 27:51Nominal rewriting and Lambda
- 31:07Nominal unification algorithms
- 36:44Complexity of nominal matching
- 41:03Alpha with equational theories
- 48:08Results and future work
- 51:24Q&A
related talks
21mUndecidability of Higher-Order Unification Formalised in Coq
29mUnification Modulo Isomorphisms between Dependent Types for Type-based Library Search
30mNominal Matching Logic With Fixpoints
28mTowards Light-Weight Operational Reasoning for Languages with Binders, Categorically
35mOmelets Need Onions: E-graphs Modulo Theories via Bottom Up E-Matching
11mLocal algebraic effect theories
18mFast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect...
14mAdequacy for Algebraic Effects Revisited