Formalized 1-category theory forms a core component of various libraries of mathematical proofs. However, more sophisticated results in fields from algebraic topology to theoretical physics, where objects have “higher structure,” rely on infinite-dimensional categories in place of 1-dimensional categories, and ∞-category theory has thusfar proved unamenable to computer formalization.

Higher-order unification (HOU) concerns unification of (extensions of) $λ$-calculus and can be seen as an instance of equational unification ($E$-unification) modulo $βη$-equivalence of $λ$-terms. We study equational unification of terms in languages with arbitrary variable binding constructions modulo arbitrary second-order equational theories. Abstract syntax with general variable binding and parametrised metavariables allows us to work with arbitrary binders without committing to $λ$-calculus or use inconvenient and error-prone term encodings, leading to a more flexible framework. In this paper, we introduce $E$-unification for second-order abstract syntax and describe a unification procedure for such problems, merging ideas from both full HOU and general $E$-unification. We prove that the procedure is sound and complete.

Many calculi exist for modeling various features of object-oriented languages. Many of them are based on λ -calculus and focus either on statically typed class-based languages or dynamic prototype-based languages. We formalize the untyped calculus of decorated objects, informally presented by Bugayenko, which is defined in terms of objects and relies on decoration as a primary mechanism of object extension. It is not based on λ -calculus, yet with only four basic syntactic constructions is just as complete (in particular, it is Turing complete and possesses the Church-Rosser property). We also provide a sound translation to Wand’s λ -calculus with records and concatenation, and discuss the key differences of these calculi.