一句话：为抽象机器提出双模型与双正交语义框架，统一证明 CK/CEK 机器的重要性质与模拟关系。
论文为抽象机器建立组合式语义，以 call-by-push-value 的 CK/CEK 机器为主要操作语义。作者引入 bimodel，为程序和栈分别提供指称，并进一步提出 environment bimodel 以处理闭包。每个模型都有句法实例（由机器构造）和集合论实例（作为指称语义）。借助双正交（biorthogonality），论文在模型上定义逻辑关系，并证明对模型与观察方式参数化的基本引理。不同实例化可导出 canonicity、adequacy、操作外延性、内部完全抽象，以及关联 CK 与 CEK 机器的一阶模拟定理。全部结果在 Agda 中机器化验证。
We develop a compositional semantics for abstract machines, focusing on CK/CEK machines for call-by-push-value. Taking abstract machines as the primary operational semantics, we introduce bimodels, which give denotations to both programs and stacks, and environment bimodels, which extend the construction to closures. Each has a syntactic instance, built from the machine itself, and a set-theoretic instance that serves as a denotational semantics. Using biorthogonality, we define logical relations over these models and prove fundamental lemmata that are parametric in the choice of model and observation. Different instantiations yield canonicity, adequacy, operational extensionality, internal full abstraction, and a first-order simulation theorem relating the CK and CEK machines. All results are mechanized in Agda.