A new approach to abstract syntax with variable binding
From MaRDI portal
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
Cited in
(only showing first 100 items - show all)- The First-Order Nominal Link
- Algebras of UTxO blockchains
- scientific article; zbMATH DE number 7649901 (Why is no real title available?)
- Functorial coalgebraic logic: the case of many-sorted varieties
- Game semantics in the nominal model
- Behavioural equivalences for dynamic web data
- Fixed-point constraints for nominal equational unification
- A lazy desugaring system for evaluating programs with sugars
- A system-level game semantics
- Nominal confluence tool
- Confluence and commutation for nominal rewriting systems with atom-variables
- Nominal syntax with atom substitutions
- Nested abstract syntax in Coq
- Permutation groups with small orbit growth
- Two-level lambda-calculus
- A library of anti-unification algorithms
- Secrecy and group creation
- Algorithmic games for full ground references
- Unranked Nominal Unification
- Formalizing adequacy: a case study for higher-order abstract syntax
- The \(\pi\)-calculus is behaviourally complete and orbit-finitely executable
- Fuzzy sets within finitely supported mathematics
- New
- Matching and alpha-equivalence check for nominal terms
- Bunched polymorphism
- Simple and subdirectly irreducible finitely supported \(Cb\)-sets
- Encoding abstract syntax without fresh names
- Formal metatheory of the lambda calculus using Stoughton's substitution
- The nominal/FM Yoneda lemma
- Two cotensors in one: presentations of algebraic theories for local state and fresh names
- αCheck: A mechanized metatheory model checker
- Reachability in pushdown register automata
- Mechanized metatheory revisited
- On a monadic semantics for freshness
- Fast computations on ordered nominal sets
- Rule formats for nominal process calculi
- Nominal Domain Theory for Concurrency
- Free functor from the category of \(G\)-nominal sets to that of 01-\(G\)-nominal sets
- Binding operators for nominal sets
- Alpha-structural induction and recursion for the lambda calculus in constructive type theory
- Properties of the atoms in finitely supported structures
- A class of automata for the verification of infinite, resource-allocating behaviours
- A simple nominal type theory
- scientific article; zbMATH DE number 7577567 (Why is no real title available?)
- A program logic for fresh name generation
- Incorporating quotation and evaluation into Church's type theory
- Deciding contextual equivalence of \(\nu \)-calculus with effectful contexts
- Distinguishing between communicating transactions
- A spatial equational logic for the applied \(\pi \)-calculus
- Proof-relevant \(\pi\)-calculus: a constructive account of concurrency and causality
- A general mathematics of names
- External and internal syntax of the \(\lambda \)-calculus
- Declarative event based models of concurrency and refinement in psi-calculi
- A formalized general theory of syntax with bindings: extended version
- Structural recursion with locally scoped names
- A name abstraction functor for named sets
- Nominal rewriting
- Alpha equivalence equalities
- On the construction of free algebras for equational systems
- Nominal equational logic
- scientific article; zbMATH DE number 1759453 (Why is no real title available?)
- Psi-calculi in Isabelle
- Broadcast psi-calculi with an application to wireless protocols
- Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
- Rule formats for nominal process calculi
- Bialgebraic methods and modal logic in structural operational semantics
- The theory of contexts for first order and higher order abstract syntax
- Viewing \({\lambda}\)-terms through maps
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- Symmetries, local names and dynamic (de)-allocation of names
- HasCasl: integrated higher-order specification and program development
- Abstract syntax: substitution and binders
- A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Unity in nominal equational reasoning: the algebra of equality on nominal sets
- Programming with algebraic effects and handlers
- scientific article; zbMATH DE number 1696799 (Why is no real title available?)
- Nominal automata for resource usage control
- Equivariant unification
- Families of symmetries as efficient models of resource binding
- Nominal techniques in Isabelle/HOL
- Computing strong and weak bisimulations for psi-calculi
- A Category of Explicit Fusions
- Nominal Lawvere theories: a category theoretic account of equational theories with names
- Nominal monoids
- A game semantics of names and pointers
- Completeness and Herbrand theorems for nominal logic
- Mechanizing type environments in weak HOAS
- Binding in nominal equational logic
- Bialgebraic methods in structural operational semantics (invited talk)
- About permutation algebras, (pre)sheaves and named sets
- Coalgebraic modal logic beyond sets
- A spatial logic for concurrency. I
- Full abstraction for Reduced ML
- Nominal logic, a first order theory of names and binding
- Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness
- Free-algebra models for the \(\pi \)-calculus
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
- The abstract variable-binding calculus
- A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
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)
