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.

翻译：我们将Fiore、Plotkin和Turi关于带绑定、替换与空缺的抽象语法处理方法，适配至包含二阶类别的语言。此类情形涵盖诸如按值调用λ演算（CBV）与Levy的按推值调用（CBPV）等程序演算体系。禁止二阶类别在变量上下文中出现，使得抽象语法的表征从幺半范畴中的幺半群转变为作用范畴中的作用结构。我们通过双范畴论证复现了该理论的大部分推导过程，并应用所得理论证明了CBV变体的替换引理。