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 (only showing first 100 items - show all)
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
Uses Software
This page was built for publication: A new approach to abstract syntax with variable binding
