Institut de Mathématiques de Marseille, UMR 7373




Rechercher


Accueil > Équipes de recherche > Logique de la Programmation (LDP) > Thèses, HDR > Agenda des soutenances

Agenda des soutenances LDP

par Lozingot Eric - publié le , mis à jour le

Agenda

Séminaire

groupe de travail

  • Vendredi 29 mars 10:00-12:00 - Guillaume GEOFFROY - I2M, AGLR-LDP, Aix-Marseille Université

    Réalisabilité classique : nouveaux outils et applications

    Résumé : Soutenance de thèse
    -
    La réalisabilité classique de Jean-Louis Krivine associe à chaque modèle de calcul et chaque modèle de la théorie des ensembles un nouveau modèle de la théorie des ensembles, appelé modèle de 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 j2 (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 correspondent au cas où j2 est réduite à l’algèbre de Boole à deux éléments.
    Ce travail présente de nouveaux outils pour manipuler les modèles de réalisabilité et donne de nouveaux résultats obtenus en les exploitant. 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 j2, 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 j2 est élémentairement équivalente à B. Deux autres résultats montrent que j2 peut être utilisée pour étudier les modèles dénotationnels de langage de programmation (chacun des deux part d’un modèle dénotationnel particulier et classifie ses degrés de parallélisme à l’aide de j2). 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 choix 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 adaptant la condition d’antichaîne dénombrable du forcing au cadre de la réalisabilité, ce qui semble semble ouvrir une piste prometteuse pour résoudre le problème de la réalisation de l’axiome du choix complet.
    -
    Mots clés : Logique, réalisabilité classique, théorie de la démonstration, sémantique dénotationnelle, lambda-calcul.
    -
    Membres du jury :
    -
    Directeur
    - Laurent Regnier - Professeur, Aix-Marseille Université
    Rapporteurs
    - Thomas Streicher (Technische Universität Darmstadt)
    - Alexandre Miquel (Montevideo, Uruguay)
    Examinateurs
    - Mirna Dzamonja (U. East Anglia, Norwich, UK)
    - Jean-Louis Krivine (Paris 7)
    - Colin Riba (ENS Lyon)
    - Nicolas Tabareau (INRIA, Nantes)
    - Matteo Viale (Turin)
    -

    JPEG - 11.7 ko
    Guillaume GEOFFROY

    -
    PNG - 7.7 ko
    (lien à venir)


    -
    Liens :
    - theses.fr
    - Fiche de l’ED184

    Lieu : Site St Charles - Aix-Marseille Université
    3, place Victor Hugo - case 39
    13331 MARSEILLE Cedex 03

    Exporter cet événement

Manifestation scientifique

-
-
Retrouvez ici les dates des soutenances ("A venir") ainsi que toutes les thèses soutenues par les doctorants de l’équipe LDP ("Archives"), depuis le 1er janvier 2014 (ou, à cette adresse, sous forme de tableau triable par équipe).