BEGIN:VCALENDAR VERSION:2.0 PRODID:-//wp-events-plugin.com//7.2.3.1//EN TZID:Europe/Paris X-WR-TIMEZONE:Europe/Paris BEGIN:VEVENT UID:7078@i2m.univ-amu.fr DTSTART;TZID=Europe/Paris:20190329T140000 DTEND;TZID=Europe/Paris:20190329T170000 DTSTAMP:20241209T195823Z URL:https://www.i2m.univ-amu.fr/evenements/realisabilite-classique-nouveau x-outils-et-applications/ SUMMARY:Guillaume Geoffroy (I2M\, Aix-Marseille Université): Réalisabilit é classique : nouveaux outils et applications DESCRIPTION:Guillaume Geoffroy: -\nRéalisabilité classique : nouveaux out ils et applications\nLa réalisabilité classique de Jean-Louis Krivine as socie à chaque modèle de calcul et chaque modèle de la théorie des ens embles un nouveau modèle de la théorie des ensembles\, appelé modèle d e réalisabilité\, d’une façon similaire au forcing. Chaque modèle de réalisabilité est muni d’une algèbre de Boole caractéristique gimel 2\, dont la structure donne des informations sur les propriétés du mod èle de réalisabilité. En particulier\, les modèles de forcing correspo ndent au cas où gimel 2 est réduite à l’algèbre de Boole à deux él éments.\n\nCe travail présente de nouveaux outils pour manipuler les mod èles de réalisabilité et donne de nouveaux résultats obtenus en les ex ploitant. L’un d’entre eux est qu’au premier ordre\, la théorie des algèbres de Boole à au moins deux éléments est complète pour gimel 2 \, au sens où pour toute algèbre de Boole B (à au moins deux éléments )\, il existe un modèle de réalisabilité dans lequel gimel 2 est élém entairement équivalente à B. Deux autres résultats montrent que gimel 2 peut être utilisée pour étudier les modèles dénotationnels de langag e de programmation (chacun des deux part d’un modèle dénotationnel par ticulier et classifie ses degrés de parallélisme à l’aide de gimel 2) . Dans le domaine de la théorie des ensembles\, un autre résultat montre que la technique de Jean-Louis Krivine pour réaliser l’axiome des choi x dépendants à partir de l’instruction quote peut se généraliser à des formes plus fortes de choix. Enfin\, un dernier résultat\, obtenu en collaboration avec Laura Fontanella\, accompagne le précédent en adaptan t la condition d’antichaîne dénombrable du forcing au cadre de la réa lisabilité\, ce qui semble semble ouvrir une piste prometteuse pour réso udre le problème de la réalisation de l’axiome du choix complet.\n\nMo ts clés : Logique\, réalisabilité classique\, théorie de la démonstra tion\, sémantique dénotationnelle\, lambda-calcul.\n\nClassical realizab ility: new tools and applications\nJean-Louis Krivine’s classical realiz ability defines\, from any given model of computation and any given model of set theory\, a new model of set theory called the realizability model\, in a similar way to forcing. Each realizability model is equipped with a c haracteristic Boolean algebra (gimel2)\, whose structure encodes important information about the properties of the realizability model. For instance \, forcing models are precisely the realizability models in which gimel 2 is the Boolean algebra with to elements.\n\nThis document defines new tool s for studying realizability models and exploits them to de-rive new resul ts. One such result is that\, as far as first-order logic is concerned\, t he theory of Boolean algebras with at least two elements is complete for g imel 2\, meaning that for each Boolean algebra B (with at least two elemen ts)\, there exists a realizability model in which gimel 2 is elementarily equivalent to B. Next\, two results show that gimel 2 can be used as a too l to study denotational models of programming languages (each one of them takes a particular denotational mode land classifies its degrees of parall elism using gimel 2). Moving to set theory\, another results generalizes J ean-Louis Krivine’s technique of realizing the axiom of dependent choice s using the instruction quote to higher forms of choice. Finally\, a last result\, which is joint work with Laura Fontanella\, complements the previ ous one by adapting the countable antichain condition from forcing to clas sical realizability\, which seems to open a new\, promising approach to th e problem of realizing the full axiom of choice.\n\nMembres du jury :\nDir ecteur\n- Laurent Regnier - Professeur\, Aix-Marseille Université\nRappor teurs\n- Thomas Streicher (Technische Universität Darmstadt)\n- Alexandre Miquel (Montevideo\, Uruguay)\n\nExaminateurs\n- Mirna Dzamonja (U. East Anglia\, Norwich\, UK)\n- Jean-Louis Krivine (Paris 7)\n- Colin Riba (ENS Lyon)\n- Nicolas Tabareau (INRIA\, Nantes)\n- Matteo Viale (Turin)\n\nLien s :\n- theses.fr\n- Fiche de l'ED184\n ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2 020/01/Guillaume_Geoffroy.jpg CATEGORIES:Soutenance de thèse,AGLR,Logique et Interactions LOCATION:Saint-Charles\, Campus Saint-Charles\, Marseille\, 13003\, France X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=Campus Saint-Charles\, Mars eille\, 13003\, France;X-APPLE-RADIUS=100;X-TITLE=Saint-Charles:geo:0,0 END:VEVENT BEGIN:VTIMEZONE TZID:Europe/Paris X-LIC-LOCATION:Europe/Paris BEGIN:STANDARD DTSTART:20181028T020000 TZOFFSETFROM:+0200 TZOFFSETTO:+0100 TZNAME:CET END:STANDARD END:VTIMEZONE END:VCALENDAR