Projects per year
Abstract
We introduce Nominal Matching Logic (NML) as an extension of Matching Logic with names and binding following the GabbayPitts 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 wellbehaved 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 metatheoretical 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 language  English 

Title of host publication  Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming (PPDP 2022) 
Publisher  ACM Association for Computing Machinery 
Number of pages  20 
ISBN (Print)  9781450397032 
DOIs  
Publication status  Published  20 Sep 2022 
Event  24th International Symposium on Principles and Practice of Declarative Programming  Tbilisi, Georgia Duration: 20 Sep 2022 → 22 Sep 2022 Conference number: 24 https://software.imdea.org/Conferences/PPDP2022/ 
Symposium
Symposium  24th International Symposium on Principles and Practice of Declarative Programming 

Abbreviated title  PPDP 2022 
Country/Territory  Georgia 
City  Tbilisi 
Period  20/09/22 → 22/09/22 
Internet address 
Keywords
 Binding operator
 Matching Logic
 Nominal Logic
 LambdaCalculus
 Verification
Fingerprint
Dive into the research topics of 'Nominal Matching Logic'. Together they form a unique fingerprint.Projects
 1 Finished

SkyeA programming language bridging theory and practice for scientific data curation
1/09/16 → 31/08/22
Project: Research