A general approach to define binders using matching logic

Xiaohong Chen; Grigore Rosu

doi:10.1145/3408970

A general approach to define binders using matching logic

Xiaohong Chen, Grigore Rosu

Research output: Contribution to journal › Article › peer-review

12 Citations (SciVal)

Original language	English
Article number	88
Journal	Proceedings of the ACM on Programming Languages
Volume	4
Issue number	ICFP
DOIs	https://doi.org/10.1145/3408970
Publication status	Published (VoR) - 2 Aug 2020

Funding

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.

Keywords

binders
completeness
conservative extension
matching logic

Access to Document

10.1145/3408970

Cite this

@article{65abc40fcd0f46c5a851b7731efaa2e1,

title = "A general approach to define binders using matching logic",

keywords = "binders, completeness, conservative extension, matching logic",

author = "Xiaohong Chen and Grigore Rosu",

note = "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{\'a}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. Publisher Copyright: {\textcopyright} 2020 Owner/Author.",

year = "2020",

month = aug,

day = "2",

doi = "10.1145/3408970",

language = "English",

volume = "4",

journal = "Proceedings of the ACM on Programming Languages",

issn = "2475-1421",

publisher = "Association for Computing Machinery (ACM)",

number = "ICFP",

}

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. Publisher Copyright: © 2020 Owner/Author.

PY - 2020/8/2

Y1 - 2020/8/2

KW - binders

KW - completeness

KW - conservative extension

KW - matching logic

UR - https://www.scopus.com/pages/publications/85090272360

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

U2 - 10.1145/3408970

DO - 10.1145/3408970

M3 - Article

AN - SCOPUS:85090272360

SN - 2475-1421

VL - 4

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - ICFP

M1 - 88

ER -

A general approach to define binders using matching logic

Funding

Keywords

Access to Document

Other files and links

Fingerprint

Cite this