Towards a unified proof framework for automated fixpoint reasoning using matching logic

Xiaohong Chen; Minh Thai Trinh; Nishant Rodrigues; Lucas Peña; Grigore Roşu

doi:10.1145/3428229

Towards a unified proof framework for automated fixpoint reasoning using matching logic

Xiaohong Chen, Minh Thai Trinh, Nishant Rodrigues, Lucas Peña, Grigore Roşu

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

5 Citations (SciVal)

Original language	English
Article number	161
Journal	Proceedings of the ACM on Programming Languages
Volume	4
Issue number	OOPSLA
DOIs	https://doi.org/10.1145/3428229
Publication status	Published (VoR) - 13 Nov 2020

Funding

We warmly thank the anonymous OOPSLA reviewers and our shepherd. Their wit and dedication has 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. This research is also partly supported by the National Research Foundation, Prime Minister’s Office, Singapore under its Campus for Research Excellence and Technological Enterprise (CREATE) programme.

Keywords

automated reasoning
fixpoints
induction
matching logic

Access to Document

10.1145/3428229

Cite this

@article{b42774c7a63244828078acec5b7b9226,

title = "Towards a unified proof framework for automated fixpoint reasoning using matching logic",

keywords = "automated reasoning, fixpoints, induction, matching logic",

author = "Xiaohong Chen and Trinh, \{Minh Thai\} and Nishant Rodrigues and Lucas Pe{\~n}a and Grigore Ro{\c s}u",

note = "Funding Information: We warmly thank the anonymous OOPSLA reviewers and our shepherd. Their wit and dedication has 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. This research is also partly supported by the National Research Foundation, Prime Minister{\textquoteright}s Office, Singapore under its Campus for Research Excellence and Technological Enterprise (CREATE) programme. Publisher Copyright: {\textcopyright} 2020 Owner/Author.",

year = "2020",

month = nov,

day = "13",

doi = "10.1145/3428229",

language = "English",

volume = "4",

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

issn = "2475-1421",

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

number = "OOPSLA",

}

TY - JOUR

T1 - Towards a unified proof framework for automated fixpoint reasoning using matching logic

AU - Chen, Xiaohong

AU - Trinh, Minh Thai

AU - Rodrigues, Nishant

AU - Peña, Lucas

AU - Roşu, Grigore

N1 - Funding Information: We warmly thank the anonymous OOPSLA reviewers and our shepherd. Their wit and dedication has 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. This research is also partly supported by the National Research Foundation, Prime Minister’s Office, Singapore under its Campus for Research Excellence and Technological Enterprise (CREATE) programme. Publisher Copyright: © 2020 Owner/Author.

PY - 2020/11/13

Y1 - 2020/11/13

KW - automated reasoning

KW - fixpoints

KW - induction

KW - matching logic

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

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

U2 - 10.1145/3428229

DO - 10.1145/3428229

M3 - Article

AN - SCOPUS:85097582718

SN - 2475-1421

VL - 4

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - OOPSLA

M1 - 161

ER -

Towards a unified proof framework for automated fixpoint reasoning using matching logic

Funding

Keywords

Access to Document

Other files and links

Fingerprint

Cite this