Séminaire, 16 octobre 2025
Programme
- 10:30 – 12:00
-
Étienne Miquey (IML, Marseille)Invited talk: Generic approaches to effectful realizability
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
- 13:45 – 14:45
-
Rafaël Bocquet (Eötvös Loránd University, Budapest, Hungary)
In algebraic approaches to the syntax and semantics of dependent type theory, the syntax is characterized as the initial object of a category of models. Then the universal property of the initial model corresponds to an induction principle over the syntax: properties of the syntax (canonicity, normalization, etc.) are proven through interpretation of the syntax into various models.
The proofs of many properties do not immediately follow from the induction principle, but require a suitable strengthening of the induction hypotheses. This is typically achieved using methods such as categorical gluing. However, constructing the corresponding model fully explicitly would be tedious, due for instance to the need to check many naturality conditions.
I will present "relative induction principles", which are stronger induction principles that can be used to more directly prove the desired properties of the syntax.
This is based on the paper "For the Metatheory of Type Theory, Internal Sconing is Enough" (joint work with Ambrus Kaposi and Christian Sattler), and on my upcoming PhD thesis "Relative Induction Principles for Second-Order Generalized Algebraic Theories".
- 15:15 – 16:15
-
Francesca Guffanti (Lama, Université Savoie Mont Blanc)
This talk aims to describe a first step toward a doctrinal approach to quantifier-free formulas and quantifier alternation depth modulo a first-order theory.
The set of quantifier-free formulas modulo a first-order theory is axiomatized by what we call a quantifier-free fragment of a Boolean doctrine with quantifiers. Rather than being an intrinsic notion, a quantifier-free fragment is an additional structure on a Boolean doctrine with quantifiers. Under a smallness assumption, the structures occurring as quantifier-free fragments of some Boolean doctrines with quantifiers are precisely the Boolean doctrines (without quantifiers). To obtain this characterization, we use the fact that every Boolean doctrine over a small base category admits a quantifier completion, of which it is a quantifier-free fragment.
Furthermore, the stratification by quantifier alternation depth of first-order formulas motivates the introduction of quantifier alternation stratified Boolean doctrines. While quantifier-free fragments are defined in relation to an “ambient” Boolean doctrine with quantifiers, a quantifier alternation stratified Boolean doctrine requires no such ambient doctrine. Indeed, it consists of a sequence of Boolean doctrines (without quantifiers) with connecting axioms. Such sequences are in one-to-one correspondence with pairs consisting of a Boolean doctrine with quantifiers and a quantifier-free fragment of it.
This talk is based on a joint work with Marco Abbadini [1].
[1] M. Abbadini, F. Guffanti. Quantifier-free formulas and quantifier alternation depth in doctrines. Journal of Pure and Applied Algebra, Volume 229, Issue 8, 2025.
