Thèse Propriétés Universelles des Systèmes de Types Algorithmiques pour les Lambda Calculs d'Ordre Supérieur H/F - 75

Établissement : Institut Polytechnique de Paris École polytechnique
École doctorale : Ecole Doctorale de l'Institut Polytechnique de Paris
Laboratoire de recherche : LIX - Laboratoire d'informatique
Direction de la thèse : Samuel MIMRAM ORCID 0000000207672569
Début de la thèse : 2026-10-01
Date limite de candidature : 2026-04-15T23:59:59Cette thèse de doctorat explore la structure catégorique des systèmes de types algorithmique, en particulier à travers la théorie des catégories fibrées. Les systèmes de types jouent un rôle central en informatique en garantissant la correction des programmes. Ils existent sous deux formes principales : déclarative (basée sur des règles) et algorithmique (basée sur des procédures de décision). Cependant, la transformation d'un système déclaratif en un système algorithmique efficace reste un défi majeur.

L'approche proposée modélise les systèmes de types comme des foncteurs, associant une catégorie des dérivations de typage aux programmes non typés. Ainsi, la vérification des types devient un problème de relèvement, ce qui relie la théorie des types à la théorie des catégories fibrées, largement utilisée en géométrie algébrique. Ce cadre permet d'analyser des concepts complexes tels que le sous-typage et les types d'intersection, tout en mettant en évidence un lien profond entre vérification de types et analyse syntaxique en langages formels.

La thèse applique cette approche au typage bidirectionnel, une méthode algorithmique qui combine vérification et inférence des types. Elle met en avant une analogie entre synthèse de type principal et relèvement cartésien dans les catégories fibrées. Les premiers travaux se concentrent sur le typage bidirectionnel pour le lambda-calcul simplement typé et son fragment linéaire, où les types principaux présentent une propriété de contractibilité. Cette propriété est également pertinente dans l'étude des catégories cartésiennes fermées et des -catégories faibles, avec des extensions possibles aux catégories monoïdales fermées supérieures.

Les travaux poursuivront également une exploration fibrée du polymorphisme et des types dépendants, en s'appuyant sur des résultats récents. Bien que ce ne soit pas le focus principal, la thèse reconnaît aussi un lien entre le typage bidirectionnel et les grammaires attribuées de Knuth, qui intègrent un raisonnement bidirectionnel en analyse syntaxique.

En exploitant la théorie des catégories, cette recherche vise à mettre en évidence les propriétés universelles des systèmes de types algorithmique, ouvrant ainsi de nouvelles perspectives pour les fondements des langages de programmation.

Les systèmes de types jouent un rôle fondamental dans la conception et la vérification des langages de programmation et des assistants de preuve. En imposant des contraintes formelles sur les programmes, ils garantissent des propriétés essentielles comme la sûreté d'exécution et l'absence de certaines erreurs. Depuis les travaux pionniers sur le lambda-calcul typé et les logiques formelles, les systèmes de types ont évolué pour répondre aux besoins croissants des langages modernes, intégrant des notions avancées telles que le polymorphisme, les types dépendants ou encore le sous-typage. Toutefois, si la spécification des systèmes de types repose souvent sur des règles déclaratives élégantes, leur mise en oeuvre algorithmique pose de nombreux défis, notamment en matière d'efficacité et de décidabilité. L'objectif de cette thèse est d'explorer ces questions sous un angle catégorique, en s'appuyant sur la théorie des catégories fibrées pour modéliser le processus algorithmique de vérification des types et dégager des principes universels qui régissent ces systèmes.

Cette thèse vise à appliquer une approche fibrée aux systèmes de types algorithmiques afin d'en identifier la structure catégorique profonde et leurs propriétés universelles. Un des objectifs majeurs est d'analyser le typage bidirectionnel, une approche qui combine vérification et synthèse des types grâce à une séparation soigneuse de ces deux modes de raisonnement.

Il existe une comparaison naturelle entre la synthèse des types, où un type principal est dérivé pour un terme dans un contexte donné, et la notion de relèvement cartésien en théorie des catégories fibrées. Cela suggère que des généralisations de la bifibration catégorique, déjà utilisées dans l'analyse de divers systèmes logiques, pourraient être appliquées avec succès au typage bidirectionnel.

Le projet débutera par l'étude du typage bidirectionnel standard pour le lambda-calcul simplement typé et son fragment strictement linéaire. Le cas linéaire présente une propriété remarquable : les types principaux sont contractibles, c'est-à-dire qu'ils admettent des habitants uniques à équivalence près. Cette notion de contractibilité a été récemment exploitée pour fournir une nouvelle présentation impartiale des catégories cartésiennes fermées, englobant la logique combinatoire et s'appuyant sur une approche issue de la théorie des types pour les -catégories faibles. Un cadre fibré solide pour le typage principal pourrait permettre d'étendre ces résultats aux catégories cartésiennes et monoïdales fermées de dimension .

En parallèle, la thèse cherchera à développer une approche fibrée du typage bidirectionnel pour le polymorphisme et les types dépendants, en s'appuyant sur des travaux récents. Bien que l'analogie entre le typage et l'analyse syntaxique ne soit pas le coeur du projet, elle pourrait offrir des pistes intéressantes. En particulier, les grammaires attribuées de Knuth intègrent une forme de raisonnement bidirectionnel qui pourrait avoir une connexion formelle avec le typage bidirectionnel. Une analyse catégorique préliminaire de ces grammaires a déjà été proposée à travers la construction Int, qui joue également un rôle dans la modélisation du lambda-calcul et de l'algèbre combinatoire linéaire.