一句话：提出用匹配逻辑统一公理化定义对象语言中的绑定器，并给出保守扩展与模型完备性结果。
论文针对不同逻辑系统中绑定器（binder）定义分散、语义处理各异的问题，提出一种基于匹配逻辑的通用定义方法。其核心思想是让对象层绑定器的绑定行为直接继承自匹配逻辑内建的 exists 绑定器，从而在匹配逻辑中把 λ 演算、System F、π 演算和纯类型系统等系统的绑定器定义为记号和逻辑理论。作者通过保守扩展定理证明这些定义的正确性：一个 sequent/judgment 在原系统中可证当且仅当在匹配逻辑对应理论中可证。该定义还为各类绑定器给出模型，这些模型对原系统形式推理是演绎完备的；对 λ 演算，模型还满足表示完备性。
We propose a novel definition of binders using matching logic, where the binding behavior of object-level binders is directly inherited from the built-in exists binder of matching logic. We show that the behavior of binders in various logical systems such as lambda-calculus, System F, pi-calculus, pure type systems, can be axiomatically defined in matching logic as notations and logical theories. We show the correctness of our definitions by proving conservative extension theorems, which state that a sequent/judgment is provable in the original system if and only if it is provable in matching logic, in the corresponding theory. Our matching logic definition of binders also yields models to all binders, which are deductively complete with respect to formal reasoning in the original systems. For lambda-calculus, we further show that the yielded models are representationally complete, a desired property that is not enjoyed by many existing lambda-calculus semantics. This work is part of a larger effort to develop a logical foundation for the programming language semantics framework K (http://kframework.org).
@article{ChenR20,
title = {A general approach to define binders using matching logic},
author = {Xiaohong Chen and Grigore Roşu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {ICFP},
year = {2020},
doi = {10.1145/3408970}
}