The First-Order Nominal Link

DOI10.1007/978-3-642-20551-4_15zbMath1326.68083OpenAlexW1481023204MaRDI QIDQ3003496

Christophe Calvès, Maribel Fernández

Publication date: 27 May 2011

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-642-20551-4_15

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (4)

Nominal syntax with atom substitutions ⋮ Completeness in PVS of a nominal unification algorithm ⋮ A formalisation of nominal C-matching through unification with protected variables ⋮ Formalising nominal C-unification generalised with protected variables

Uses Software

• OCaml
• Freshml

Cites Work

• Unnamed Item
• A new approach to abstract syntax with variable binding
• A polynomial nominal unification algorithm
• Nominal unification
• Nominal logic, a first order theory of names and binding
• Nominal rewriting
• Nominal Equational Logic
• Nominal Matching and Alpha-Equivalence
• Nominal (Universal) Algebra: Equational Logic with Names and Binding
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Unification of higher-order patterns in linear time and space
• FreshML
• An Efficient Nominal Unification Algorithm
• Nominal Unification from a Higher-Order Perspective

This page was built for publication: The First-Order Nominal Link