A new approach to abstract syntax with variable binding

DOI10.1007/s001650200016zbMath1001.68083MaRDI QIDQ699761

Andrew M. Pitts, Murdoch James Gabbay

Publication date: 25 September 2002

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s001650200016

zbMATH Keywords

set theory; permutation actions; abstract syntax; alpha-conversion; structural induction

Mathematics Subject Classification ID

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

18B20: Categories of machines, automata

03E99: Set theory

Related Items

Completeness and Herbrand theorems for nominal logic, About permutation algebras, (pre)sheaves and named sets, A coalgebraic approach to the semantics of the ambient calculus, A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names., Secrecy and group creation, Nominal unification, Nominal logic, a first order theory of names and binding, A spatial logic for concurrency. I, Fresh logic: Proof-theory and semantics for FM and nominal techniques, Nominal rewriting, A general mathematics of names, On a monadic semantics for freshness, Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts

Uses Software

• Isabelle