一句话：提出 Evidenced Frames 框架，统一并拓宽可实现性模型，使 realizer 本身可带状态、非确定性与失败等效应。
构造性基础依赖高阶逻辑与类型论的可实现性模型，但传统模型对计算刻画有限，主要支持非终止，难容纳状态、非确定性与失败等效应；已有工作多以幂集等外部结构表示非确定性，而 realizer 仍确定。本文提出 Evidenced Frames：一个构建可实现性模型的通用框架，通过使底层结构更灵活来支持多样效应计算。该框架允许 realizer 自身具有效应，如可操作状态、非确定归约或直接失败的 λ 项。作者证明它是高阶依赖谓词逻辑可实现性模型的统一框架，相对这些模型完备，且 implicative algebras 的完备性构造可经该更简单构造分解得到。这表明 Evidenced Frames 可作为统一并拓宽可实现性模型的理想领域。
Constructive foundations have for decades been built upon realizability models for higher-order logic and type theory. However, traditional realizability models have a rather limited notion of computation, which only supports non-termination and avoids many other commonly used effects. Work to address these limitations has typically overlaid structure on top of existing models, such as by using powersets to represent non-determinism, but kept the realizers themselves deterministic. This paper alternatively addresses these limitations by making the structure underlying realizability models more flexible. To this end, we introduce evidenced frames: a general-purpose framework for building realizability models that support diverse effectful computations. We demonstrate that this flexibility permits models wherein the realizers themselves can be effectful, such as λ-terms that can manipulate state, reduce non-deterministically, or fail entirely. Beyond the broader notions of computation, we demonstrate that evidenced frames form a unifying framework for (realizability) models of higher-order dependent predicate logic. In particular, we prove that evidenced frames are complete with respect to these models, and that the existing completeness construction for implicative algebras-another foundational framework for realizability-factors through our simpler construction. As such, we conclude that evidenced frames offer an ideal domain for unifying and broadening realizability models.