Nominal Matching Logic with Fixpoints
Pages 17 - 33
Abstract
Matching logic is the foundation of the K semantic environment for the specification of programming languages and automated generation of evaluators and verification tools. NLML is a formalization of nominal logic, which facilitates specification and reasoning about languages with binders, as a matching logic theory. Many properties of interest are inductive, and to prove them an induction principle modulo alpha-equality is required. In this paper we show that an alpha-structural Induction Principle for any nominal binding signature can be derived in an extension of NLML with set variables and fixpoint operators. We illustrate the use of the principle to prove properties of the λ-calculus, the computation model underlying functional programming languages. The techniques generalize to other languages with binders. The proofs have been written in and generated using Metamath Zero.
References
[1]
Mario Carneiro. 2020. Metamath Zero: Designing a theorem prover prover. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings 13. Springer, 71-88.
[2]
Xiaohong Chen, Dorel Lucanu, and Grigore Roşu. 2021. Matching logic explained. Journal of Logical and Algebraic Methods in Programming 120 ( 2021 ), 100638. https://doi.org/10.1016/j.jlamp. 2021.100638
[3]
Xiaohong Chen and Grigore Rosu. 2019. Matching-Logic. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019. 1-13. https://doi.org/10.1109/ LICS. 2019.8785675
[4]
Xiaohong Chen and Grigore Rosu. 2020. A general approach to define binders using matching logic. Proc. ACM Program. Lang. 4, ICFP ( 2020 ), 88 : 1-88 : 32. https://doi.org/10.1145/3408970
[5]
James Cheney and Maribel Fernández. 2022. Nominal Matching Logic. In PPDP 2022: 24th International Symposium on Principles and Practice of Declarative Programming, Tbilisi, Georgia, September 20-22, 2022. ACM, 5 : 1-5 : 15. https://doi.org/10.1145/3551357.3551375
[6]
Murdoch J. Gabbay and Andrew M. Pitts. 2001. A New Approach to Abstract Syntax with Variable Binding. Formal Aspects of Computing 13, 3-5 ( July 2001 ), 341-363.
[7]
Norman D. Megill. 2019. Metamath: A Computer Language for Mathematical Proofs. Lulu Press, Morrisville, North Carolina. http://us.metamath.org/downloads/metamath.pdf.
[8]
Andrew M. Pitts. 2001. Nominal Logic: A First Order Theory of Names and Binding. In TACS (LNCS, Vol. 2215 ). Springer, 219-242.
[9]
Andrew M. Pitts. 2003. Nominal Logic, A First Order Theory of Names and Binding. Inf. Comput. 186, 2 ( 2003 ), 165-193.
[10]
Andrew M. Pitts. 2013. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, USA.
[11]
Grigore Roşu. 2017. Matching logic. Logical Methods in Computer Science 13, 4 ( December 2017 ), 1-61. https://doi.org/abs/1705.06312
[12]
Nishant Rodrigues, Mircea Octavian Sebe, Xiaohong Chen, and Grigore Roşu. 2024. A Logical Treatment of Finite Automata. In Tools and Algorithms for the Construction and Analysis of Systems, Bernd Finkbeiner and Laura Kovács (Eds.). Springer Nature Switzerland, Cham, 350-369.
[13]
Octavian Mircea Sebe. [n. d.]. NLML formalization. https://doi.org/10. 1145/3580443
[14]
Christian Urban. 2008. Nominal Techniques in Isabelle/HOL. J. Autom. Reason. 40, 4 (May 2008 ), 327-356.
[15]
Christian Urban, Stefan Berghofer, and Michael Norrish. 2007. Barendregt's Variable Convention in Rule Inductions. In Automated Deduction-CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings (Lecture Notes in Computer Science, Vol. 4603 ), Frank Pfenning (Ed.). Springer, 35-50. https://doi.org/10.1007/978-3-540-73595-3_4
Index Terms
- Nominal Matching Logic with Fixpoints
Recommendations
Nominal Matching Logic
PPDP '22: Proceedings of the 24th International Symposium on Principles and Practice of Declarative ProgrammingWe 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 framework, used to specify programming languages and automatically ...
Nominal logic programming
Nominal logic is an extension of first-order logic which provides a simple foundation for formalizing and reasoning about abstract syntax modulo consistent renaming of bound names (that is, α-equivalence). This article investigates logic programming ...
Interactive Matching Logic Proofs in Coq
Theoretical Aspects of Computing – ICTAC 2023AbstractMatching logic (ML) is a formalism for specifying and reasoning about mathematical structures by means of patterns and pattern matching. Previously, it has been used to capture a number of other logics, e.g., separation logic with recursive ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2025
298 pages
ISBN:9798400713477
DOI:10.1145/3703595
- General Chairs:
- Kathrin Stark,
- Amin Timany,
- Program Chairs:
- Sandrine Blazy,
- Nicolas Tabareau
Copyright © 2025 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Sponsors
In-Cooperation
- SIGLOG: SIGLOG
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 10 January 2025
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Funding Sources
- Royal Society
Conference
CPP '25
Sponsor:
CPP '25: 14th ACM SIGPLAN International Conference on Certified Programs and Proofs
January 20 - 21, 2025
CO, Denver, USA
Acceptance Rates
Overall Acceptance Rate 18 of 26 submissions, 69%
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 68Total Downloads
- Downloads (Last 12 months)68
- Downloads (Last 6 weeks)68
Reflects downloads up to 18 Feb 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in