一句话：提出用于代价感知指称语义的元语言，为 STLC 与 Modernized Algol 构造合成模型并证明代价感知计算充分性。
本文研究如何在依赖类型论中合成地开发代价感知的指称语义及其元理论。作者扩展 Niu 等人关于代价与行为验证的工作，定义了两个表达力递进的元语言，用于建立代价感知的指称模型。他们为简单类型 λ 演算以及带一阶存储和 while 循环的 Modernized Algol 构造合成指称模型，并证明其满足经典 Plotkin 型计算充分性定理的代价感知推广。由于证明在区分内涵构造与外延构造的相分离合成语言中完成，相应结果可自然限制为外延定理。该工作正面回答了原工作提出的猜想，并提供了面向代价感知编程、验证与元理论的框架。
We present metalanguages for developing synthetic cost-aware denotational semantics of programming languages. Extending recent advances by Niu et al. in cost and behavioral verification in dependent type theory, we define two successively more expressive metalanguages for studying cost-aware metatheory. We construct synthetic denotational models of the simply-typed lambda calculus and Modernized Algol, a language with first-order store and while loops, and show that they satisfy a cost-aware generalization of the classic Plotkin-type computational adequacy theorem. Moreover, by developing our proofs in a synthetic language of phase-separated constructions of intension and extension, our results easily restrict to the corresponding extensional theorems. Consequently, our work provides a positive answer to the conjecture raised in op. cit. and contributes a framework for cost-aware programming, verification, and metatheory.