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

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.

• Publication year

  2025

• Venue

  Mathematical Foundations of Programming Semantics

• Publication date

  2025-11-06

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.46298/entics.16879arXiv 2511.03946
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Abstract Operational Methods for Call-by-Push-Value

  2024cited by this paper
• An Introduction to Different Approaches to Initial Semantics

  2024cited by this paper
• From Thin Concurrent Games to Generalized Species of Structures

  2023cited by this paper
• Stabilized profunctors and stable species of structures

  2023cited by this paper
• Formal metatheory of second-order abstract syntax

  2022cited by this paper
• What Makes a Strong Monad?

  2022cited by this paper
• Towards a Higher-Order Mathematical Operational Semantics

  2022cited by this paper
• Variable binding and substitution for (nameless) dummies

  2022cited by this paper
• Implementing a category-theoretic framework for typed abstract syntax

  2021cited by this paper
• Abstract clones for abstract syntax

  2021cited by this paper
• Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention

  2021cited by this paper
• Modules over Monads and Operational Semantics

  2020cited by this paper
• Mechanising syntax with binders in Coq

  2020cited by this paper
• A Cellular Howe Theorem

  2020cited by this paper
• Coq à la carte: a practical approach to modular syntax with binders

  2020cited by this paper
• Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions

  2019cited by this paper
• Bindings as bounded natural functors

  2019cited by this paper
• POPLMark reloaded: Mechanizing proofs by logical relations

  2019cited by this paper
• Everybody's Got To Be Somewhere

  2018cited by this paper
• Generic Description of Well-Scoped, Well-Typed Syntaxes

  2018influential reference
• A type and scope safe universe of syntaxes with binding: their semantics and proofs

  2018cited by this paper
• Intrinsically-typed definitional interpreters for imperative languages

  2017cited by this paper
• List Objects with Algebraic Structure

  2017cited by this paper
• Needle & Knot: Binder Boilerplate Tied Up

  2016cited by this paper
• Syntax and Semantics of Abstract Binding Trees

  2016cited by this paper
• Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures

  2016influential reference
• Completeness and Decidability of de Bruijn Substitution Algebra in Coq

  2015cited by this paper
• Unguarded Recursion on Coinductive Resumptions

  2014cited by this paper
• Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic

  2013cited by this paper
• Automatically Generated Infrastructure for De Bruijn Syntaxes

  2013cited by this paper
• Generic conversions of abstract syntax representations

  2012cited by this paper
• Skew-monoidal categories and bialgebroids

  2012cited by this paper
• The Locally Nameless Representation

  2012cited by this paper
• Strongly Typed Term Representations in Coq

  2012cited by this paper
• GMeta: A Generic Formal Metatheory Framework for First-Order Representations

  2012cited by this paper
• The representational adequacy of Hybrid

  2011cited by this paper
• Modules over relative monads for syntax and semantics

  2011cited by this paper
• Binders unbound

  2011cited by this paper
• Modules over monads and initial semantics

  2010cited by this paper
• The span construction

  2010cited by this paper
• Equational properties of iterative monads

  2010cited by this paper
• Initial Algebra Semantics for Cyclic Sharing Structures

  2009cited by this paper
• A Framework for Specifying, Prototyping, and Reasoning about Computational Systems

  2009cited by this paper
• A unified framework for generalized multicategories

  2009cited by this paper
• A Two-Level Logic Approach to Reasoning About Computations

  2009cited by this paper
• Data types à la carte

  2008cited by this paper
• Second-Order and Dependently-Sorted Abstract Syntax

  2008influential reference
• Parametric higher-order abstract syntax for mechanized semantics

  2008cited by this paper
• The cartesian closed bicategory of generalised species of structures

  2008cited by this paper
• Engineering formal metatheory

  2008cited by this paper
• Mechanized Metatheory for the Masses: The PoplMark Challenge

  2005cited by this paper
• Toward a general theory of names: binding and scope

  2005cited by this paper
• Exploring the Regular Tree Types

  2004influential reference
• Infinite trees and completely iterative theories: a coalgebraic view

  2003cited by this paper
• Call-By-Push-Value: A Functional/Imperative Synthesis

  2003cited by this paper
• Abstract Syntax and Variable Binding (Extended Abstract)

  2003cited by this paper
• Higher Operads, Higher Categories

  2003cited by this paper
• A New Approach to Abstract Syntax with Variable Binding

  2002cited by this paper
• Extensible algebraic datatypes with defaults

  2001cited by this paper
• Semantics of name and value passing

  2001cited by this paper
• Axioms for Recursion in Call-by-Value

  2001cited by this paper
• Implementing Extensible Compilers

  2001cited by this paper
• Complete axioms for categorical fixed-point operators

  2000cited by this paper
• Semantical analysis of higher-order abstract syntax

  1999cited by this paper
• Call-by-Push-Value: A Subsuming Paradigm

  1999cited by this paper
• fc-multicategories

  1999cited by this paper
• Monadic Presentations of Lambda Terms Using Generalized Inductive Types

  1999cited by this paper
• Synthesizing Object-Oriented and Functional Design to Promote Re-Use

  1998cited by this paper
• Towards a mathematical operational semantics

  1997cited by this paper
• User-defined types and procedural data structures as complementary approaches to data abstraction

  1994cited by this paper
• Iteration Theories: The Equational Logic of Iterative Processes

  1993cited by this paper
• Object-Oriented Programming Versus Abstract Data Types

  1990cited by this paper
• Higher-order abstract syntax

  1988cited by this paper
• Monadic Computation And Iterative Algebraic Theories

  1982cited by this paper
• Initial Algebra Semantics and Continuous Algebras

  1977cited by this paper
• Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem

  1972cited by this paper
• Monads on symmetric monoidal closed categories

  1970cited by this paper
• Under Consideration for Publication in J. Functional Programming Ott: Effective Tool Support for the Working Semanticist

  year unknowncited by this paper

• No citing papers are available for this paper.