Modular abstract syntax trees (MAST): substitution tensors with second-class sorts
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866914358154493952 |
|---|---|
| author | Fiore, Marcelo P. Kammar, Ohad Moser, Georg Staton, Sam |
| author_facet | Fiore, Marcelo P. Kammar, Ohad Moser, Georg Staton, Sam |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_03946 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Modular abstract syntax trees (MAST): substitution tensors with second-class sorts Fiore, Marcelo P. Kammar, Ohad Moser, Georg Staton, Sam Programming Languages 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. |
| title | Modular abstract syntax trees (MAST): substitution tensors with second-class sorts |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2511.03946 |