Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax

DOI10.2178/bsl/1305810911zbMath1253.03059OpenAlexW2127052734MaRDI QIDQ3011103

Murdoch James Gabbay

Publication date: 28 June 2011

Published in: The Bulletin of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2178/bsl/1305810911

zbMATH Keywords

survey papernominal techniquesvariable bindingnamesalpha-equivalencenominal abstract syntaxatoms-abstractioninductive syntax up to binding

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40)

Related Items (15)

Nominal lambda calculus: an internal language for FM-Cartesian closed categories ⋮ Formal metatheory of the lambda calculus using Stoughton's substitution ⋮ Nominal Kleene Coalgebra ⋮ Game Semantics in the Nominal Model ⋮ Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free ⋮ Completeness and incompleteness in nominal Kleene algebra ⋮ Order algebras: a quantitative model of interaction ⋮ αCheck: A mechanized metatheory model checker ⋮ Unity in nominal equational reasoning: the algebra of equality on nominal sets ⋮ Alpha equivalence equalities ⋮ Nominal Automata with Name Binding ⋮ PNL to HOL: from the logic of nominal sets to the logic of higher-order functions ⋮ Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness ⋮ Denotational Semantics with Nominal Scott Domains ⋮ Coalgebraic semantics for nominal automata

Uses Software

• Freshml

Cites Work

• Nominal techniques in Isabelle/HOL
• Capture-avoiding substitution as a nominal algebra
• A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets
• Substitution revisited
• About \({|}/{|}\)-quantifiers
• A spatial logic for concurrency. II
• Nominal logic, a first order theory of names and binding
• Avoiding the axiom of choice in general category theory
• Fresh logic: Proof-theory and semantics for FM and nominal techniques
• A general mathematics of names
• On a monadic semantics for freshness
• Alpha-structural recursion and induction
• Completeness and Herbrand theorems for nominal logic
• THE INDEPENDENCE OF THE CONTINUUM HYPOTHESIS
• Proceedings of the eighth ACM SIGPLAN international conference on Functional programming

This page was built for publication: Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax