Espaces topologiques de types et de termes – TopTT

La logique est un thème en commun à la fois à la théorie des automates et à l'étude des langages de programmation. En théorie des automates et des circuits, la logique est typiquement utilisée comme un formalisme descriptif pour classifier les classes de complexité. Dans l'étude des langages de programmation par le biais de la théorie des preuves, la logique est utilisée principalement pour raisonner sur les propriétés comportementales de systèmes de calcul, telles que leur utilisation des ressources, ou leur traitement des fonctions d'ordre supérieur et des points fixes.

Ce projet utilisera des méthodes topologiques profinies pour développer une base commune pour ces deux utilisations distinctes de la logique. En particulier, la dualité de Stone fournit un cadre topologique pour étudier les espaces de types et de termes canoniquement associés à une spécification logique. Elle peut donc être appliquée indépendamment du formalisme de machine sous-jacent, qu'il soit plutôt basé sur les automates ou sur les calculs de preuve. Ainsi, le calcul des espaces topologiques des types et des termes associés à une logique conduit à de nouvelles méthodes sémantiques.

L'objectif principal de ce projet est d'obtenir de nouveaux résultats dans la séparation des classes de complexité des circuits via une application de cette méthodologie profinie à la sémantique faisceautique des logiques d'ordre supérieur. De manière plus générale, en combinant les méthodes fondamentales de deux domaines, différents en apparence, la recherche proposée ici renforcera l'utilisation des méthodes topologiques en fondements de l'informatique.