Foundations of nominal techniques: logic and semantics of variables in abstract syntax

DOI10.2178/BSL/1305810911MaRDI QIDQ3011103zbMATH OpenOpenAlexFDO

Authors Murdoch J. 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

alpha-equivalenceatoms-abstractioninductive syntax up to bindingnamesnominal abstract syntaxnominal techniquessurvey papervariable binding

Mathematics Subject Classification ID

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

Recommendations

• A new approach to abstract syntax with variable binding
• scientific article; zbMATH DE number 2242589
• Nominal logic, a first order theory of names and binding
• Nominal (universal) algebra: equational logic with names and binding
• Fresh logic: Proof-theory and semantics for FM and nominal techniques

Cites work

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

Cited in

(24)

• Variables and scopes considered formally
• Coalgebraic semantics for nominal automata
• Formal metatheory of the lambda calculus using Stoughton's substitution
• Encoding abstract syntax without fresh names
• Completeness and incompleteness in nominal Kleene algebra
• Nominal lambda calculus: an internal language for FM-Cartesian closed categories
• On the role of names in reasoning about -tree syntax specifications
• A dependent nominal type theory
• Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free
• Nominal automata with name binding
• Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables
• Game semantics in the nominal model
• Nominal Kleene coalgebra
• Unity in nominal equational reasoning: the algebra of equality on nominal sets
• Alpha equivalence equalities
• Order algebras: a quantitative model of interaction
• αCheck: A mechanized metatheory model checker
• Equivariant ZFA and the foundations of nominal techniques
• Leaving the nest: nominal techniques for variables with interleaving scopes
• Denotational semantics with nominal Scott domains
• Equational reasoning modulo commutativity in languages with binders
• Nominal Henkin semantics: simply-typed lambda-calculus models in nominal sets
• 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

Describes a project that uses

Uses Software

• FreshML

This page was built for publication: Foundations of nominal techniques: logic and semantics of variables in abstract syntax

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3011103)