Évènement

Félix Castro
I2M, Aix-Marseille
https://www.irif.fr/users/castro/index

Date(s) : 12/02/2026   iCal
11h00 - 12h30

In Kleene realizability, formulas are interpreted as sets of
(untyped) programs. This approach allows for a sound interpretation of
Higher-Order Logic (HOL): it leads to the definition of the effective
topos and, more generally, to a wide range of toposes obtained from
« partial combinatory algebras ». All these realizability toposes have
an important common feature: they arise from an untyped model of
computations.

On the other hand, typed programming languages were also used to
design realizability models. Notably, Paulin-Mohring extended Kreisel
modified realizability to the Calculus of Constructions (CC), thus
giving a typed realizability interpretation of HOL. It is therefore
natural to ask whether one can build toposes from such typed
interpretations. Unfortunately, the answer is negative: Lietz and
Streicher showed that the (Set-based) categorical models coming from a
« typed partial combinatory algebra » are impredicative only if it is
essentially untyped.

It seems unsatisfactory to me: if a typed programming language is
strong enough to interpret HOL, it should be possible to obtain
directly an impredicative categorical model from it! During this talk,
we will work internally in an extension of CC to build an « evidenced
frame » from (a variation of) Paulin-Mohring model and without
degenerating the type system of the calculus at stake. Because
triposes can be built from evidenced frames, this work is a first step
toward an answer of the title question: no, typed realizability is not
only (categorically) predicative!

Emplacement
I2M Luminy - TPR2, Salle de Séminaire 304-306 (3ème étage)

Catégories

• Séminaire