Marcelo P. Fiore ; Ohad Kammar ; Georg Moser ; Sam Staton
-
Modular abstract syntax trees (MAST): substitution tensors with second-class sorts
entics:16879 -
Electronic Notes in Theoretical Informatics and Computer Science,
December 20, 2025,
Volume 5 - Proceedings of MFPS XLI
-
https://doi.org/10.46298/entics.16879Modular abstract syntax trees (MAST): substitution tensors with second-class sortsArticle
Authors: Marcelo P. Fiore ; Ohad Kammar ; Georg Moser ; Sam Staton
NULL##NULL##NULL##NULL
Marcelo P. Fiore;Ohad Kammar;Georg Moser;Sam Staton
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.
Volume: Volume 5 - Proceedings of MFPS XLI
Published on: December 20, 2025
Accepted on: November 11, 2025
Submitted on: November 7, 2025
Keywords: Programming Languages