A new approach to abstract syntax with variable binding
From MaRDI portal
Publication:699761
DOI10.1007/s001650200016zbMath1001.68083OpenAlexW1975082667MaRDI 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
Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Categories of machines, automata (18B20) Set theory (03E99)
Related Items
Nominal lambda calculus: an internal language for FM-Cartesian closed categories, Formal metatheory of the lambda calculus using Stoughton's substitution, Declarative event based models of concurrency and refinement in psi-calculi, Relating Coalgebraic Notions of Bisimulation, A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle, 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, Binding in Nominal Equational Logic, A Nominal Relational Model for Local Store, New, Game Semantics in the Nominal Model, A System-Level Game Semantics, Model checking Petri nets with names using data-centric dynamic systems, A program logic for fresh name generation, Nominal Automata for Resource Usage Control, About permutation algebras, (pre)sheaves and named sets, Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free, Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts, Algorithmic games for full ground references, Families of Symmetries as Efficient Models of Resource Binding, A coalgebraic approach to the semantics of the ambient calculus, Encoding abstract syntax without fresh names, Formalizing adequacy: a case study for higher-order abstract syntax, Reachability in pushdown register automata, A lazy desugaring system for evaluating programs with sugars, Nominal syntax with atom substitutions, Nominal monoids, A Library of Anti-unification Algorithms, Full abstraction for Reduced ML, Simple and subdirectly irreducible finitely supported \(Cb\)-sets, Equivariant unification, Symmetries, local names and dynamic (de)-allocation of names, Mechanizing type environments in weak HOAS, A Category of Explicit Fusions, Ugo Montanari and Software Verification, A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names., Unity in nominal equational reasoning: the algebra of equality on nominal sets, Nominal Matching and Alpha-Equivalence, Nested abstract syntax in Coq, Alpha equivalence equalities, Distinguishing between communicating transactions, Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax, Computing strong and weak bisimulations for psi-calculi, Block structure vs scope extrusion: between innocence and omniscience, Program equivalence in a simple language with state, Pure Pointer Programs with Iteration, Nominal techniques in Isabelle/HOL, Nominal Lawvere theories: a category theoretic account of equational theories with names, Programming with algebraic effects and handlers, Algorithmic Nominal Game Semantics, Capture-avoiding substitution as a nominal algebra, The First-Order Nominal Link, A formalized general theory of syntax with bindings: extended version, Binding operators for nominal sets, Alpha-structural induction and recursion for the lambda calculus in constructive type theory, Structural recursion with locally scoped names, Behavioural equivalences for dynamic web data, Free-algebra models for the \(\pi \)-calculus, A game semantics of names and pointers, Incorporating quotation and evaluation into Church's type theory, Regular and context-free nominal traces, Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms, Secrecy and group creation, External and internal syntax of the \(\lambda \)-calculus, Matching and alpha-equivalence check for nominal terms, PNL to HOL: from the logic of nominal sets to the logic of higher-order functions, A spatial equational logic for the applied \(\pi \)-calculus, Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness, Fuzzy sets within finitely supported mathematics, Permutation groups with small orbit growth, Properties of the atoms in finitely supported structures, Free functor from the category of \(G\)-nominal sets to that of 01-\(G\)-nominal sets, A Simple Nominal Type Theory, Two Cotensors in One: Presentations of Algebraic Theories for Local State and Fresh Names, A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets, HasCasl: integrated higher-order specification and program development, Viewing \({\lambda}\)-terms through maps, A Class of Automata for the Verification of Infinite, Resource-Allocating Behaviours, A congruence rule format for name-passing process calculi, Bialgebraic methods and modal logic in structural operational semantics, On the construction of free algebras for equational systems, Nominal Confluence Tool, Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables, Broadcast Psi-calculi with an Application to Wireless Protocols, A Sorted Semantic Framework for Applied Process Calculi (Extended Abstract), Mechanizing the Metatheory of mini-XQuery, Mechanized metatheory revisited, The Theory of Contexts for First Order and Higher Order Abstract Syntax, The lambda-context calculus (extended version), On a monadic semantics for freshness, Nominal Equational Logic, Bialgebraic Methods in Structural Operational Semantics, A Name Abstraction Functor for Named Sets, Functorial Coalgebraic Logic: The Case of Many-sorted Varieties, Contextual equivalence for inductive definitions with binders in higher order typed functional programming, Confluence and commutation for nominal rewriting systems with atom-variables, On nominal sets with support-preorder, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Algebras of UTxO blockchains, Unnamed Item, When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus, The fresh-graph of a nominal set, αCheck: A mechanized metatheory model checker, Deciding contextual equivalence of \(\nu \)-calculus with effectful contexts, Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting, Active learning for deterministic bottom-up nominal tree automata, Nominal Sets in Agda - A Fresh and Immature Mechanization, Nominal AC-matching, The reflective higher-order calculus: encodability, typability and separation, Unnamed Item, Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and Applications, Psi-calculi revisited: connectivity and compositionality, Reasoning about multi-stage programs, Psi-calculi in Isabelle, Unnamed Item, Unnamed Item, Fixed-Point Constraints for Nominal Equational Unification, Bunched polymorphism, Generic Authenticated Data Structures, Formally., a-Logic With Arrows, Proof-Relevant Logical Relations for Name Generation, Hard Life with Weak Binders, Towards Nominal Abramsky, Fast computations on ordered nominal sets, Proof-relevant π-calculus: a constructive account of concurrency and causality, Unnamed Item, Full Abstraction for Reduced ML, Completeness and Herbrand theorems for nominal logic, Nominal Domain Theory for Concurrency, Term Sequent Logic, Two-level Lambda-calculus, The nominal/FM Yoneda Lemma, Unnamed Item, Coverability Synthesis in Parametric Petri Nets, Denotational Semantics with Nominal Scott Domains, Abstract Syntax: Substitution and Binders, Coalgebraic Modal Logic Beyond Sets, A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
Uses Software
