Nominal Matching Logic With Fixpoints

Watch this 30-minute conference talk from CPP 2025 where researchers Mircea Sebe, Maribel Fernandez, and James Cheney present their work on Nominal Matching Logic with Fixpoints. Explore how they extend Nominal Logic Matching Logic (NLML) with set variables and fixpoint operators to derive an alpha-structural Induction Principle for nominal binding signatures. Learn how this principle can be applied to prove properties of the λ-calculus and other languages with binders. The presentation demonstrates how their techniques, verified using Metamath Zero, provide a foundation for the K semantic environment used in programming language specification and automated verification tool generation. Access the full article and supplementary artifacts to deepen your understanding of formal verification approaches for languages with binding operators.