TY - JOUR

T1 - A general approach to define binders using matching logic

AU - Chen, Xiaohong

AU - Rosu, Grigore

N1 - Funding Information:
We warmly thank the K Team for invaluable and continuous feedback on matching logic and its role as a foundation of K, as well as for their creative yet hard work on turning theoretical results into practical tools. We also warmly thank James Cheney, Maribel Fernández, Andrei Popescu, and Thomas Tuegel for many insightful comments and concrete suggestions. We are indebted to the four anonymous reviewers, whose wit and dedication helped us improve the presentation. This work was supported in part by NSF CNS 16-19275. This material is based upon work supported by the United States Air Force and DARPA under Contract No. FA8750-18-C-0092.

PY - 2020/8/2

Y1 - 2020/8/2

N2 - 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).

AB - 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).

KW - binders

KW - completeness

KW - conservative extension

KW - matching logic

UR - http://www.scopus.com/inward/record.url?scp=85090272360&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85090272360&partnerID=8YFLogxK

U2 - 10.1145/3408970

DO - 10.1145/3408970

M3 - Article

AN - SCOPUS:85090272360

VL - 4

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

SN - 2475-1421

IS - ICFP

M1 - 88

ER -