Axe transverse LOGIQUES du LIRMM

Journée SOUS TYPAGE 

(organisée par Vincent Blazy et Christian Retoré)

Mardi 10 décembre 2024 10h-17h

LIRMM batiment 5 salle 1.124




Un sous type d'un type en programmation fonctionnelle typée est un peu comme comme une classe fille d'une autre classe en programmation objet. Intégrer la notion de sous typage à un système de typage fonctionnelle basé sur la logique n'est pas aisé,car cette notions doit se propager dans les types fonctionnels (X->Y: type des fonctions du type X dans le type Y) et en notant A<B pour "A est un sous type de B" la règle de sous typage est si A<B et V<U alors (U->A) < (V->B)

La première tentative d'un système logique de types est sans doute celle de Luca Cardelli au milieu des années 1990 avec "F omega" appelée "F omega sub", mais le systèmes résultant était très compliqué. Dans les années 2000 Sergeï Soloviev (IRIT) a introduit le sous typage coercitif qui requiert qu'il n'y ait qu'une seule fonction de A' dans A quand A'<A cela s'intègre beaucoup mieux dans un système de types de nature logique que le sous typage de Cardelli.

Depuis les travaux de Soloviev, les chercheurs du domaine ont cherché à intégrer le sous typage coercitif dans diverses théorie des types comme la théorie des types de Martin-Löf (Luo, Soloviev), le calcul des constructions de Coquand Huet (Vincent Blazy), le system F (Retoré), et à implémenter cette notion de sous typage dans le prouveur interactif Coq.

Outre l'application évidente en programmation fonctionnelle, le sous typage coercitif d'applique aussi à la sémantique du langage naturel standard exprimée en lambda calcul typé: les coercions lexicales correspondant à des inclusions ontologiques sont vue avec succès comme un phénomène de sous typage (Asher, Chatzikyriakidis, Gotham, Luo, Méry, Moot, Retoré...).


Programme (détails à venir)