Journal article
Modular abstract syntax trees (MAST): substitution tensors with second-class sorts
- 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.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Version of record, pdf, 569.1KB, Terms of use)
-
- Publisher copy:
- 10.46298/entics.16879
- Publication website:
- https://core.ac.uk/download/736115472.pdf
Authors
- Publisher:
- Institut de recherche en informatique et en automatique
- Journal:
- Electronic Notes in Theoretical Informatics and Computer Science More from this journal
- Volume:
- Volume 5 - Proceedings of...
- Article number:
- 16879
- Publication date:
- 2025-12-20
- Acceptance date:
- 2025-11-11
- DOI:
- EISSN:
-
2969-2431
- ISSN:
-
2969-2431
- Language:
-
English
- Keywords:
- Pubs id:
-
2493974
- Local pid:
-
pubs:2493974
- Source identifiers:
-
W4417525543
- Deposit date:
-
2026-11-07
- ARK identifier:
This ORA record was generated from metadata provided by an external service. It has not been edited by the ORA Team.
Terms of use
- Copyright date:
- 2025
- Licence:
- CC Attribution-ShareAlike (CC BY-SA)
If you are the owner of this record, you can report an update to it here: Report update to this record