Generic approaches to effectful realizability

Salón 102 de la FIng.

Aunque el título y resumen estén en inglés, la charla será en
español.


Abstract:
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  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) [2], 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] From Partial to Monadic : Combinatory Algebras with Effect. Cohen,
Grünfeld, Kirst & Miquey. FSCD 2025
_________________