A Certified Functional Nominal C-Unification Algorithm
From MaRDI portal
Publication:5097631
DOI10.1007/978-3-030-45260-5_8zbMath1502.68145OpenAlexW3020665690MaRDI QIDQ5097631
Gabriel Ferreira Silva, Maribel Fernández, Mauricio Ayala-Rincón, Daniele Nantes-Sobrinho
Publication date: 25 August 2022
Published in: Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-030-45260-5_8
Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42)
Related Items (2)
Rewriting with generalized nominal unification ⋮ Formalising nominal C-unification generalised with protected variables
Cites Work
- Unnamed Item
- Unnamed Item
- Complete axiomatizations of some quotient term algebras
- Nominal techniques in Isabelle/HOL
- A polynomial nominal unification algorithm
- Nominal C-unification
- Completeness in PVS of a nominal unification algorithm
- A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols
- Nominal unification
- Nominal rewriting
- Nominal unification of higher order expressions with recursive let
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
- Nominal Sets
- Term Rewriting and All That
- Fixed-Point Constraints for Nominal Equational Unification
- Nominal Anti-Unification
- Logic Programming
- An Efficient Nominal Unification Algorithm
- (Nominal) Unification by Recursive Descent with Triangular Substitutions
- Nominal Unification from a Higher-Order Perspective
This page was built for publication: A Certified Functional Nominal C-Unification Algorithm
