A new approach to abstract syntax with variable binding

DOI10.1007/S001650200016zbMATH Open1001.68083OpenAlexW1975082667MaRDI QIDQ699761FDOQ699761

Authors: Andrew M. Pitts, Murdoch J. 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

Recommendations

• scientific article; zbMATH DE number 1696799
• scientific article; zbMATH DE number 1759453
• The abstract variable-binding calculus
• A syntactic abstraction for rule-based languages with binding
• A unified treatment of syntax with binders
• Abstract syntax: substitution and binders
• A conservative look at operational semantics with variable binding
• A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
• A lambda-calculus for dynamic binding

zbMATH Keywords

set theoryabstract syntaxalpha-conversionpermutation actionsstructural induction

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Categories of machines, automata (18B20) Set theory (03E99)

Cited In (only showing first 100 items - show all)

• Nominal confluence tool
• Deciding contextual equivalence of \(\nu \)-calculus with effectful contexts
• Nominal Domain Theory for Concurrency
• Confluence and commutation for nominal rewriting systems with atom-variables
• Matching and alpha-equivalence check for nominal terms
• Properties of the atoms in finitely supported structures
• Formal metatheory of the lambda calculus using Stoughton's substitution
• Mechanized metatheory revisited
• Binding operators for nominal sets
• Alpha-structural induction and recursion for the lambda calculus in constructive type theory
• A library of anti-unification algorithms
• Reachability in pushdown register automata
• Incorporating quotation and evaluation into Church's type theory
• A spatial equational logic for the applied \(\pi \)-calculus
• A system-level game semantics
• Unranked Nominal Unification
• Proof-relevant \(\pi\)-calculus: a constructive account of concurrency and causality
• Algebras of UTxO blockchains
• Behavioural equivalences for dynamic web data
• Secrecy and group creation
• A program logic for fresh name generation
• Permutation groups with small orbit growth
• Algorithmic games for full ground references
• Two cotensors in one: presentations of algebraic theories for local state and fresh names
• The First-Order Nominal Link
• Functorial coalgebraic logic: the case of many-sorted varieties
• Game semantics in the nominal model
• On a monadic semantics for freshness
• Title not available (Why is that?)
• A lazy desugaring system for evaluating programs with sugars
• Nominal syntax with atom substitutions
• Title not available (Why is that?)
• The \(\pi\)-calculus is behaviourally complete and orbit-finitely executable
• A simple nominal type theory
• αCheck: A mechanized metatheory model checker
• Fast computations on ordered nominal sets
• Rule formats for nominal process calculi
• Free functor from the category of \(G\)-nominal sets to that of 01-\(G\)-nominal sets
• Formalizing adequacy: a case study for higher-order abstract syntax
• Encoding abstract syntax without fresh names
• Simple and subdirectly irreducible finitely supported \(Cb\)-sets
• New
• Nested abstract syntax in Coq
• Fuzzy sets within finitely supported mathematics
• Distinguishing between communicating transactions
• Two-level lambda-calculus
• Fixed-point constraints for nominal equational unification
• Bunched polymorphism
• The nominal/FM Yoneda lemma
• A class of automata for the verification of infinite, resource-allocating behaviours
• Title not available (Why is that?)
• The theory of contexts for first order and higher order abstract syntax
• A spatial logic for concurrency. I
• Regular and context-free nominal traces
• Nominal lambda calculus: an internal language for FM-Cartesian closed categories
• A name abstraction functor for named sets
• Alpha equivalence equalities
• Viewing \({\lambda}\)-terms through maps
• Declarative event based models of concurrency and refinement in psi-calculi
• Bialgebraic methods in structural operational semantics (invited talk)
• Unity in nominal equational reasoning: the algebra of equality on nominal sets
• A Category of Explicit Fusions
• A congruence rule format for name-passing process calculi
• PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
• Algorithmic nominal game semantics
• A formalized general theory of syntax with bindings
• Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
• A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• The lambda-context calculus (extended version)
• A formalized general theory of syntax with bindings: extended version
• Capture-avoiding substitution as a nominal algebra
• Abstract syntax: substitution and binders
• Computing strong and weak bisimulations for psi-calculi
• Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness
• Foundations of nominal techniques: logic and semantics of variables in abstract syntax
• Title not available (Why is that?)
• Binding in nominal equational logic
• Coalgebraic modal logic beyond sets
• Nominal logic, a first order theory of names and binding
• A game semantics of names and pointers
• Model checking Petri nets with names using data-centric dynamic systems
• Broadcast psi-calculi with an application to wireless protocols
• Completeness and Herbrand theorems for nominal logic
• A sorted semantic framework for applied process calculi (extended abstract)
• Nominal unification
• Active learning for deterministic bottom-up nominal tree automata
• Program equivalence in a simple language with state
• External and internal syntax of the \(\lambda \)-calculus
• Rule formats for nominal process calculi
• Equivariant unification
• A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
• A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
• Symmetries, local names and dynamic (de)-allocation of names
• Nominal Lawvere theories: a category theoretic account of equational theories with names
• Mechanizing type environments in weak HOAS
• Free-algebra models for the \(\pi \)-calculus
• On the construction of free algebras for equational systems
• Families of symmetries as efficient models of resource binding
• A coalgebraic approach to the semantics of the ambient calculus

Uses Software

• Isabelle

This page was built for publication: A new approach to abstract syntax with variable binding

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