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é...).
10:00 Vincent Blazy (LIRMM) La question du sous typage et ses différentes modélisations
11:30 Pierre Letouzey (IRIF, Paris) Typage et sous typage des
programmes fonctionnels certifiés extraits de preuves en Coq
14:15 Vincent Blazy (LIRMM) Sous typage explicite d'univers en calcul des constructions
15:00 Richard Moot (LIRMM) et Christian Retoré (LIRMM) Sous typage dans le système F de Girard et applications en sémantique du langage naturel