Une géométrie de calcul : Réseaux de preuve, appel-par-pousse-valeur et topologie du consensus
A geometry of calculus
par Jules CHOUQUET sous la direction de Christine TASSON et de Lionel VAUX
Thèse de doctorat en Mathématiques. Logique et fondements de l'informatique
ED 386 Sciences Mathematiques de Paris Centre

Soutenue le vendredi 06 décembre 2019 à Université de Paris (2019-....)

Sujets
  • Lambda-calcul
  • Logique de seuil
  • Probabilités
  • Théorie de la démonstration
  • Topologie
  • Traitement réparti

Les thèses de doctorat soutenues à Université de Paris sont déposées au format électronique

Consultation de la thèse sur d’autres sites :

Theses.fr

Description en anglais
Description en français
Mots clés
Développement de Taylor, Appel-par-pousse-valeur, Réseaux de preuve
Resumé
L'informatique fondamentale et de la théorie de la démonstration. Deux approches sont menées : la première consiste à examiner les mécanismes d'approximation multilinéaires dans des systèmes issus du λ-calcul et de la Logique Linéaire. La seconde consiste à étudier les modèles topologiques pour les systèmes distribués et à les adapter aux algorithmes probabilistes. On étudie d'abord le développement de Taylor des réseaux de preuve de la Logique Linéaire. On introduit des méthodes de démonstration qui utilisent la géométrie de l'élimination des coupures des réseaux multiplicatifs, et qui permettent de manipuler des sommes infinies de réseaux de façon sûre et correcte, pour en extraire des propriétés sur les réductions qui sont à l'œuvre. Ensuite, nous introduisons un langage permettant de définir le développement de Taylor syntaxique pour l'Appel-Par-Pousse-Valeur (Call-By-Push-Value), en capturant certaines propriétés de la sémantique dénotationelle liées aux morphismes de coalgèbres. Puis nous nous intéressons aux systèmes distribués (à mémoire partagée, tolérants aux pannes), et au problème du Consensus. On utilise un modèle topologique qui permet d'interpréter la communication dans les complexes simpliciaux, eton l'adapte de façon à transformer les résultats d'impossibilité bien connus en résultats de borne inférieure de probabilité pour des algorithmes probabilistes