Abstract Syntax: Substitution and Binders

DOI10.1016/j.entcs.2007.02.024zbMath1316.68035OpenAlexW1968062295MaRDI QIDQ5262926

A. John Power

Publication date: 10 July 2015

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2007.02.024

zbMATH Keywords

substitutioninitial algebra semanticspseudo-distributive lawbinding signature

Mathematics Subject Classification ID

Theory of programming languages (68N15) Abstract data types; algebraic specification (68Q65) Theories (e.g., algebraic theories), structure, and semantics (18C10) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40)

Related Items (4)

Variable binding and substitution for (nameless) dummies ⋮ Variable binding and substitution for (nameless) dummies ⋮ Unnamed Item ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A new approach to abstract syntax with variable binding
• Category theory for operational semantics
• Pseudo-distributive laws and axiomatics for variable binding
• Algebraic operations and generic effects
• Pseudo-commutative monads and pseudo-closed 2-categories
• Nominal logic, a first order theory of names and binding
• The semantics and proof theory of the logic of bunched implications
• Capture-Avoiding Substitution as a Nominal Algebra
• Alpha-structural recursion and induction
• A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
• A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on
• On bunched typing
• FreshML
• Theorem Proving in Higher Order Logics
• A Unified Category-theoretic Semantics for Binding Signatures in Substructural Logics

This page was built for publication: Abstract Syntax: Substitution and Binders