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. Nonetheless, many recent works have shown how realizability models could benefit from side effects to provide computational interpretation for logic principles. In earlier work with Cohen and Tate [1], we addressed the challenge of finding a uniform and generic algebraic framework encompassing (effectful) realizability models, introducing evidenced frames for this purpose. These structures not only enable a factorization of the usual construction of a realizability topos from a tripos—evidenced frames are complete with respect to triposes—but are also flexible enough to accommodate a wide range of effectful models.

We pursued this along two main directions:

• first, by extending the syntactic (typed) approach to realizability, following Kreisel’s tradition, where propositions from a ground logic (e.g., HOL) are translated into specifications and typed programs (realizers) that satisfy them. We introduce EffHOL [2], a new framework that expands syntactic realizability. It combines higher-kinded polymorphism—enabling typing of realizers for higher-order propositions—with a computational term language using monads to represent and reason about effectful computations.

• second, by generalizing the traditional notion of Partial Combinatory Algebras (PCAs), which underpins classical realizability models. To better internalize a broad spectrum of computational effects, we propose the concept of Monadic Combinatory Algebras (MCAs) [3], in which the combinatory algebra is structured over an underlying computational effect captured by a monad. As we shall see, MCAs provide a smooth generalization of traditional PCA-based realizability semantics.

[1] Evidenced Frames: A Unifying Framework Broadening Realizability Models. Cohen, Miquey & Tate. LICS 2021

[2] Syntactic Effectful Realizability in Higher-Order Logic. Cohen, Grünfeld, Kirst & Miquey., LICS 2025

[3] From Partial to Monadic : Combinatory Algebras with Effect. Cohen, Grünfeld, Kirst & Miquey. FSCD 2025