一句话：提出广义元变量语法与范畴语义，证明特定条件下 Miller 模式合一算法可推广，并用 Agda 实现。
本文研究二阶合一的判定片段——Miller 的模式合一，并为其提出一种带元变量语法的推广。作者用范畴语义刻画这种语法，给出使 Miller 合一算法仍可适用的条件，从而把可判定性从简单类型 λ 演算扩展到更一般的签名结构，包括有序 λ 演算和 System F 等内蕴多态语法。虽然不显式处理方程，但通过在正规形式上工作，仍覆盖简单类型 λ 演算模 βη 等式这一原始设定。作者还在 Agda 中实现了通用合一算法，以说明该语义分析的有效性。
Abstract We propose a notion of syntax with metavariables that generalises Miller’s decidable pattern fragment of second-order unification for simply typed $\lambda$ -calculus. Using categorical semantics, we show that, under some conditions, a generalisation of Miller’s unification algorithm applies. To illustrate our semantic analysis, we implemented our generic unification algorithm in Agda. The syntax with metavariables given as input of the algorithm is specified by a notion of signature generalising binding signatures, covering a wide range of examples, including ordered $\lambda$ -calculus and (intrinsic) polymorphic syntax such as System F. Although we do not explicitly handle equations, we also tackle simply typed $\lambda$ -calculus modulo $\beta$ - and $\eta$ -equations (Miller’s original setting) by working on the syntax of normal forms.