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变体的替换引理。