Modular abstract syntax trees (MAST): substitution tensors with second-class sorts

2025/11/06 by Marcelo Fiore, Ohad Kammar, Fiore, Marcelo P. +5
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Programming Languages (cs.PL) #semigroups and automata theory

paper · pdf · doi:10.48550/arxiv.2511.03946

openalex publication_date 2025/11/06 · openalex created_date 2025/11/08 · openalex updated_date 2026/07/31

Abstract

We adapt Fiore, Plotkin, and Turi's treatment of abstract syntax with binding, substitution, and holes to account for languages with second-class sorts. These situations include programming calculi such as the Call-by-Value lambda-calculus (CBV) and Levy's Call-by-Push-Value (CBPV). Prohibiting second-class sorts from appearing in variable contexts changes the characterisation of the abstract syntax from monoids in monoidal categories to actions in actegories. We reproduce much of the development through bicategorical arguments. We apply the resulting theory by proving substitution lemmata for varieties of CBV.

Citations

• An Introduction to Different Approaches to Initial Semantics
• Towards a Higher-Order Mathematical Operational Semantics
• A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics\n and Proofs
• Generic Description of Well-Scoped, Well-Typed Syntaxes
• Syntax and Semantics of Abstract Binding Trees
• A two-level logic approach to reasoning about computations
• A Framework for Specifying, Prototyping, and Reasoning about Computational Systems
• Higher Operads, Higher Categories
• fc-multicategories

Related

• Syntax and Semantics of Abstract Binding Trees
• Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution
• Adjunction As Substitution: An Algebraic Formulation of Regular, Context-Free and Tree Adjoining Languages
• Substitution for Non-Wellfounded Syntax with Binders through Monoidal Categories
• Substitution Without Copy and Paste