A general approach to define binders using matching logic

Xiaohong Chen, Grigore Rosu

Research output: Contribution to journalArticlepeer-review

Abstract

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

Original languageEnglish (US)
Article number88
JournalProceedings of the ACM on Programming Languages
Volume4
Issue numberICFP
DOIs
StatePublished - Aug 2 2020

Keywords

  • binders
  • completeness
  • conservative extension
  • matching logic

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality

Fingerprint Dive into the research topics of 'A general approach to define binders using matching logic'. Together they form a unique fingerprint.

Cite this