A new approach to abstract syntax with variable binding
From MaRDI portal
(Redirected from Publication:699761)
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)- Free-algebra models for the \(\pi \)-calculus
- On the construction of free algebras for equational systems
- Pure Pointer Programs with Iteration
- Families of symmetries as efficient models of resource binding
- scientific article; zbMATH DE number 7649901 (Why is no real title available?)
- A coalgebraic approach to the semantics of the ambient calculus
- A simple nominal type theory
- The \(\pi\)-calculus is behaviourally complete and orbit-finitely executable
- Block structure vs scope extrusion: between innocence and omniscience
- Nominal rewriting
- About permutation algebras, (pre)sheaves and named sets
- Free functor from the category of G-nominal sets to that of 01-G-nominal sets
- Programming with algebraic effects and handlers
- αCheck: A mechanized metatheory model checker
- Rule formats for nominal process calculi
- Full Abstraction for Reduced ML
- Nominal equational logic
- Fast computations on ordered nominal sets
- Formalizing adequacy: a case study for higher-order abstract syntax
- Encoding abstract syntax without fresh names
- A general mathematics of names
- Structural recursion with locally scoped names
- Simple and subdirectly irreducible finitely supported \(Cb\)-sets
- HasCasl: integrated higher-order specification and program development
- Probability monads with submonads of deterministic states
- Nominal techniques in Isabelle/HOL
- Reasoning about multi-stage programs
- New
- On nominal sets with support-preorder
- Psi-calculi in Isabelle
- Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free
- Encodability and separation for a reflective higher-order calculus
- Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables
- Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
- Relating coalgebraic notions of bisimulation. With applications to name-passing process calculi (extended abstract)
- Nominal monoids
- Nested abstract syntax in Coq
- The abstract variable-binding calculus
- Nominal Matching and Alpha-Equivalence
- Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting
- Fuzzy sets within finitely supported mathematics
- Distinguishing between communicating transactions
- Two-level lambda-calculus
- Fresh logic: Proof-theory and semantics for FM and nominal techniques
- Full abstraction for Reduced ML
- scientific article; zbMATH DE number 89006 (Why is no real title available?)
- Nominal automata for resource usage control
- Fixed-point constraints for nominal equational unification
- Nominal Sets in Agda - A Fresh and Immature Mechanization
- Nominal AC-matching
- The reflective higher-order calculus: encodability, typability and separation
- Bunched polymorphism
- Bialgebraic methods and modal logic in structural operational semantics
- Contextual equivalence for inductive definitions with binders in higher order typed functional programming
- Mechanizing the metatheory of mini-XQuery
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- A class of automata for the verification of infinite, resource-allocating behaviours
- Term sequent logic
- The nominal/FM Yoneda lemma
- The theory of contexts for first order and higher order abstract syntax
- A spatial logic for concurrency. I
- scientific article; zbMATH DE number 1759453 (Why is no real title available?)
- Nominal lambda calculus: an internal language for FM-Cartesian closed categories
- Regular and context-free nominal traces
- A name abstraction functor for named sets
- Alpha equivalence equalities
- Viewing \({\lambda}\)-terms through maps
- Denotational semantics with nominal Scott domains
- Nominal confluence tool
- Declarative event based models of concurrency and refinement in psi-calculi
- Deciding contextual equivalence of \(\nu \)-calculus with effectful contexts
- Bialgebraic methods in structural operational semantics (invited talk)
- Unity in nominal equational reasoning: the algebra of equality on nominal sets
- Nominal Domain Theory for Concurrency
- Confluence and commutation for nominal rewriting systems with atom-variables
- Matching and alpha-equivalence check for nominal terms
- A Category of Explicit Fusions
- Variable binding and substitution for (nameless) dummies
- Properties of the atoms in finitely supported structures
- Formal metatheory of the lambda calculus using Stoughton's substitution
- Binding operators for nominal sets
- Alpha-structural induction and recursion for the lambda calculus in constructive type theory
- A congruence rule format for name-passing process calculi
- Mechanized metatheory revisited
- scientific article; zbMATH DE number 7136664 (Why is no real title available?)
- Towards nominal Abramsky
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
- A library of anti-unification algorithms
- Reachability in pushdown register automata
- A formalized general theory of syntax with bindings
- Algorithmic nominal game semantics
- A generic type system for higher-order \(\Psi\)-calculi
- Generic Authenticated Data Structures, Formally.
- A spatial equational logic for the applied \(\pi \)-calculus
- Incorporating quotation and evaluation into Church's type theory
- When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus
- Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets
- A system-level game semantics
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)
