Equational reasoning modulo commutativity in languages with binders

DOI10.1007/978-3-031-99984-0_33MaRDI QIDQ6869923zbMATH OpenFDO

Authors Ali K. Caires-Santos, Maribel Fernández, Daniele Nantes-Sobrinho

Publication date 21 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-99984-0_33

zbMATH Keywords

equational theorieslanguages with bindersunification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• A calculus of mobile processes. I
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A new approach to abstract syntax with variable binding
• Equational reasoning modulo commutativity in languages with binders
• Equivariant unification
• Explicit substitutions
• Formalising nominal C-unification generalised with protected variables
• Foundations of nominal techniques: logic and semantics of variables in abstract syntax
• General bindings and alpha-equivalence in Nominal Isabelle
• scientific article; zbMATH DE number 475362 (Why is no real title available?)
• Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification
• Logic Programming
• Nominal (universal) algebra: equational logic with names and binding
• Nominal AC-matching
• Nominal Algebra and the HSP Theorem
• Nominal sets. Names and symmetry in computer science
• Nominal unification
• Nominal Unification and Matching of Higher Order Expressions with Recursive Let
• Nominal unification from a higher-order perspective
• On nominal syntax and permutation fixed points
• On solving nominal fixpoint equations
• Programming with higher-order logic.
• Semantics Out of Context
• Strong nominal semantics for fixed-point constraints
• The locally nameless representation
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• The undecidability of the second-order unification problem
• Theorem Proving in Higher Order Logics

Cited in

(1)

• Equational reasoning modulo commutativity in languages with binders

This page was built for publication: Equational reasoning modulo commutativity in languages with binders

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6869923)