一句话：提出一类具体层模型，统一概率与可微编程等语义，并证明通用计算充分性定理。
本文研究带递归的按值调用高阶语言的指称语义。作者提出“具体层（concrete sheaf）模型”族，将概率编程、可微编程以及完全抽象逻辑关系模型等文献中的例子统一为特例。处理递归时采用合成域论（synthetic domain theory）的思路：从层范畴的 site 上一类可允许单态射出发，一般性地构造 lifting 单子，从而得到由具体 site 和单态射类参数化的模型族。主要结果是证明该模型族满足通用的计算充分性（computational adequacy）定理，即操作语义与指称语义在观察上一致。这为多种效应语言提供统一语义框架。
We study concrete sheaf models for a call-by-value higher-order language with recursion. Our family of sheaf models is a generalization of many examples from the literature, such as models for probabilistic and differentiable programming, and fully abstract logical relations models. We treat recursion in the spirit of synthetic domain theory. We provide a general construction of a lifting monad starting from a class of admissible monomorphisms in the site of the sheaf category. In this way, we obtain a family of models parametrized by a concrete site and a class of monomorphisms, for which we prove a general computational adequacy theorem.