Nominal Matching Logic

James Cheney, Maribel Fernández

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We introduce Nominal Matching Logic (NML) as an extension of Matching Logic with names and binding following the Gabbay-Pitts nominal approach. Matching logic is the foundation of the $\mathbb{K}$ framework, used to specify programming languages and automatically derive associated tools (compilers, debuggers, model checkers, program verifiers). Matching logic does not include a primitive notion of name binding, though binding operators can be represented via an encoding that internalises the graph of a function from bound names to expressions containing bound names. This approach is sufficient to represent computations involving binding operators, but has not been reconciled with support for inductive reasoning over syntax with binding (e.g., reasoning over $\lambda$-terms). Nominal logic is a formal system for reasoning about names and binding, which provides well-behaved and powerful principles for inductive reasoning over syntax with binding, and NML inherits these principles. We discuss design alternatives for the syntax and the semantics of NML, prove meta-theoretical properties and give examples to illustrate its expressive power. In particular, we show how induction principles for $\lambda$-terms ($\alpha$-structural induction) can be defined and used to prove standard properties of the $\lambda$-calculus.
Original languageEnglish
Title of host publicationProceedings of the 24th International Symposium on Principles and Practice of Declarative Programming (PPDP 2022)
PublisherACM Association for Computing Machinery
Number of pages20
ISBN (Print)978-1-4503-9703-2
DOIs
Publication statusPublished - 20 Sep 2022
Event24th International Symposium on Principles and Practice of Declarative Programming - Tbilisi, Georgia
Duration: 20 Sep 202222 Sep 2022
Conference number: 24
https://software.imdea.org/Conferences/PPDP2022/

Symposium

Symposium24th International Symposium on Principles and Practice of Declarative Programming
Abbreviated titlePPDP 2022
Country/TerritoryGeorgia
CityTbilisi
Period20/09/2222/09/22
Internet address

Keywords

  • Binding operator
  • Matching Logic
  • Nominal Logic
  • Lambda-Calculus
  • Verification

Fingerprint

Dive into the research topics of 'Nominal Matching Logic'. Together they form a unique fingerprint.

Cite this