Nominal Equational Logic

DOI10.1016/j.entcs.2007.02.009zbMath1277.68043OpenAlexW2094947480MaRDI QIDQ2864152

Ranald Clouston, Andrew M. Pitts

Publication date: 6 December 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

equational logicpermutation actionsuniversal algebranominal sets

Mathematics Subject Classification ID

Theory of programming languages (68N15) Logic in computer science (03B70) Equational logic, Mal'tsev conditions (08B05)

Related Items

Nominal lambda calculus: an internal language for FM-Cartesian closed categories ⋮ Binding in Nominal Equational Logic ⋮ Unnamed Item ⋮ Nominal syntax with atom substitutions ⋮ Unity in nominal equational reasoning: the algebra of equality on nominal sets ⋮ Nominal Matching and Alpha-Equivalence ⋮ Nominal Lawvere theories: a category theoretic account of equational theories with names ⋮ The First-Order Nominal Link ⋮ Equational presentations of functors and monads ⋮ On universal algebra over nominal sets ⋮ Term Equational Systems and Logics ⋮ A dependent type theory with abstractable names ⋮ Matching and alpha-equivalence check for nominal terms ⋮ Two Cotensors in One: Presentations of Algebraic Theories for Local State and Fresh Names ⋮ Nominal Unification from a Higher-Order Perspective ⋮ On the construction of free algebras for equational systems ⋮ The nominal/FM Yoneda Lemma ⋮ The lambda-context calculus (extended version) ⋮ Coverability Synthesis in Parametric Petri Nets

Uses Software

• Freshml

Cites Work

• Unnamed Item
• Unnamed Item
• Lambda abstraction algebras: representation theorems
• Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads
• A new approach to abstract syntax with variable binding
• Variations on algebra: Monadicity and generalisations of equational theories
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Substitution revisited
• Sheaves in geometry and logic: a first introduction to topos theory
• A calculus of mobile processes. II
• On the algebraic models of lambda calculus
• Nominal unification
• Nominal logic, a first order theory of names and binding
• Fresh logic: Proof-theory and semantics for FM and nominal techniques
• One-and-a-halfth-order Logic
• Alpha-structural recursion and induction
• A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
• FreshML
• Computer Science Logic
• Logic Programming
• Theorem Proving in Higher Order Logics
• Completeness and Herbrand theorems for nominal logic
• Foundations of Software Science and Computational Structures