Abstract syntax: substitution and binders

DOI10.1016/J.ENTCS.2007.02.024zbMATH Open1316.68035OpenAlexW1968062295MaRDI QIDQ5262926FDOQ5262926

Authors 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) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40) Theories (e.g., algebraic theories), structure, and semantics (18C10) Abstract data types; algebraic specification (68Q65)

Recommendations

• A Unified Category-theoretic Semantics for Binding Signatures in Substructural Logics
• Pseudo-distributive laws and axiomatics for variable binding
• scientific article; zbMATH DE number 1759453
• Typed Lambda Calculi and Applications
• scientific article; zbMATH DE number 5360218

Cites work

• scientific article; zbMATH DE number 4165146 (Why is no real title available?)
• scientific article; zbMATH DE number 5360218 (Why is no real title available?)
• scientific article; zbMATH DE number 3522196 (Why is no real title available?)
• scientific article; zbMATH DE number 1759453 (Why is no real title available?)
• scientific article; zbMATH DE number 3384258 (Why is no real title available?)
• A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
• A Unified Category-theoretic Semantics for Binding Signatures in Substructural Logics
• A new approach to abstract syntax with variable binding
• A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on
• Algebraic operations and generic effects
• Alpha-structural recursion and induction
• Capture-Avoiding Substitution as a Nominal Algebra
• Category theory for operational semantics
• FreshML: programming with binders made simple
• Nominal logic, a first order theory of names and binding
• On bunched typing
• Pseudo-commutative monads and pseudo-closed 2-categories
• Pseudo-distributive laws and axiomatics for variable binding
• The semantics and proof theory of the logic of bunched implications
• Theorem Proving in Higher Order Logics

Cited in

(13)

• Variable binding and substitution for (nameless) dummies
• A new approach to abstract syntax with variable binding
• scientific article; zbMATH DE number 1759453 (Why is no real title available?)
• Variable Binding, Symmetric Monoidal Closed Theories, and Bigraphs
• Programming Languages and Systems
• scientific article; zbMATH DE number 7559272 (Why is no real title available?)
• Pseudo-distributive laws and axiomatics for variable binding
• Heterogeneous substitution systems revisited
• Variable binding and substitution for (nameless) dummies
• Typed Lambda Calculi and Applications
• scientific article; zbMATH DE number 7577567 (Why is no real title available?)
• A Unified Category-theoretic Semantics for Binding Signatures in Substructural Logics
• scientific article; zbMATH DE number 5360218 (Why is no real title available?)

This page was built for publication: Abstract syntax: substitution and binders

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5262926)