Sara ROUSTA
Spécialité : Informatique
Laboratoire : LIPN
Directrice de thèse : Micaela Mayero
Co-encadrant : Jonas Frey
Titre de la thèse : Topologie des triposes
Les topos de réalisabilité sont des univers mathématiques alternatifs où logique et calcul sont intimement liés. Le topos effectif, issu de la réalisabilité numérique de Kleene, qui relie la logique intuitionniste — logique de l’information — à la calculabilité — étude des procédures effectives —, en est un exemple central. Dans cet univers, des énoncés frappants comme « toutes les fonctions sont calculables » deviennent vrais. Déterminer ce qui relève du seul topos effectif et ce qui découle de principes généraux de la réalisabilité exige une bonne axiomatisation. Les tripos sont de plus en plus vus comme la charpente générale de la réalisabilité.
Les tripos ont aussi une dimension topologique. Ils généralisent les locales, espaces décrits par leurs régions plutôt que par leurs points. Les locales s’inscrivent naturellement dans le monde des tripos, ce qui invite à étudier ces derniers comme des espaces généralisés. Certaines constructions, telles que les groupes, pourraient avoir des analogues triposiques. Ce n’est pas automatique : le passage des espaces topologiques aux locales ne préserve pas les produits, et les groupes définis sur des locales diffèrent déjà des groupes topologiques ordinaires. Comprendre ce qui subsiste, ce qui change et pourquoi est au cœur du projet. Certaines constructions seront aussi formalisées dans l’assistant de preuve Rocq.
Thesis title : Topology of Triposes
Realizability toposes are alternative mathematical universes in which logic and computation are intimately intertwined. The Effective topos, built from Kleene’s number realizability joining intuitionistic logic, the logic of information, to computability, the study of effective procedures, is a central example. In this universe, striking statements such as “all functions are computable” are just true. Now wanting to know how much of that behaviour is specific to the effective topos and how much of it comes from general principles of realizability calls for a good axiomatization. Triposes are increasingly seen as the underlying blueprint of realizability.
Triposes also have a topological face. They generalize locales, spaces described through their regions rather than their individual points. Locales sit naturally inside the world of triposes. Taking this seriously invites us to view triposes as generalized spaces and to investigate their topological properties. Many constructions that make sense for locales may have triposic analogues; for instance triposic groups. This is not automatic. Passing from topological spaces to locales does not preserve products, so localic groups already differ from ordinary topological groups. Understanding what survives, what changes, and why is a worthwhile part of this project. Selected constructions will also be formalized in the proof assistant Rocq.
Contactez-nous !
Campus de Villetaneuse
@univ_SPN