A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols

DOI10.1016/j.entcs.2017.04.003zbMath1401.68273OpenAlexW2660788664WikidataQ113317598 ScholiaQ113317598MaRDI QIDQ1744440

Maribel Fernández, Washington de Carvalho-Segundo, Daniele Nantes-Sobrinho, Mauricio Ayala-Rincón

Publication date: 23 April 2018

Full work available at URL: https://doi.org/10.1016/j.entcs.2017.04.003

zbMATH Keywords

nominal logicalpha equivalenceequivalence modulo A and AC

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Logic in computer science (03B70)

Related Items (6)

Unnamed Item ⋮ Nominal Unification and Matching of Higher Order Expressions with Recursive Let ⋮ A Certified Functional Nominal C-Unification Algorithm ⋮ A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols ⋮ Fixed-Point Constraints for Nominal Equational Unification ⋮ A formalisation of nominal C-matching through unification with protected variables

Uses Software

• Coq
• Isabelle/HOL
• PVS
• Freshml
• Nominal Isabelle
• Maude-NPA

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• Nominal techniques in Isabelle/HOL
• Matching and alpha-equivalence check for nominal terms
• Complexity of matching problems
• Completeness in PVS of a nominal unification algorithm
• Alpha-structural induction and recursion for the lambda calculus in constructive type theory
• Nominal unification
• Nominal rewriting
• Implementing Nominal Unification
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• FreshML
• Computer Science Logic
• (Nominal) Unification by Recursive Descent with Triangular Substitutions
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols