Nominal Matching Logic With Fixpoints
summary
Extends nominal matching logic by adding mu fixed-point operator and set variables to derive an alpha-structural induction principle for any nominal binding signature, then formalizes the whole development in Metamath Zero. Builds a nominal-matching theory of the λ-calculus, proves a nontrivial substitution identity by induction from the fixed-point axioms, and ships machine-checked proofs and artifacts. The method generates induction principles for other binder-heavy languages and the Metamath Zero files are available for inspection.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 3:04Matching logic foundations
- 7:15Nominal logic constructs
- 10:10Previous work
- 11:57Induction in matching logic
- 14:47Current work with fixpoints
- 19:02Formalization challenges
- 26:32Future work
- 27:57Q&A
related talks
15mTowards a Unified Proof Framework for Automated Fixpoint Reasoning using Matching Logic
59mUnification Modulo Equational Theories in Languages with Binding Operators
28mTowards Light-Weight Operational Reasoning for Languages with Binders, Categorically
01h 03mMatching Logic: Foundation of the K Framework
21mChecking Equivalence in a Non-strict Language
23mBetter Defunctionalization through Lambda Set Specialization
29mA Term Matching Algorithm and Substitution Generality
45mLogic Meta Programming for Functional Languages