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

TL;DR

This paper extends the theory of abstract syntax with binding to handle languages with second-class sorts, such as CBV lambda calculus and CBPV, using categorical methods and proving relevant substitution lemmas.

Contribution

It introduces a new categorical framework for abstract syntax with second-class sorts, adapting existing theories to account for variable context restrictions.

Findings

Reformulation of abstract syntax as actions in actegories for second-class sorts

Development of bicategorical arguments to support the theory

Proofs of substitution lemmas for CBV variants

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.