Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
Cette thèse propose une repréesentation de la notion de type, avec un intérêt particulier pour les types d'ependants, en Ludique.La Ludique est une th'eorie introduite par Girard. Elle vient d'une fine analyse du fragment multiplicative, additive polarisé de la Logique Linéaire (MALL_p). Un des ses buts est de reconstruire la logique à partir de la notion d'intéraction. Un type est une classe d'objets qui se comportent de la m^eme fac{c}on par rapport aux autres objets. La notion de type est commune à plusieurs domaines comme la Théorie de la Calculabilité, la Sémantique des Jeux et la Théorie Intuitioniste de Types de Martin-Lof. Avec la terminologie de Martin-Lof, le termes canoniques d'un type sont les éléments primitives du type, c'est à dire les objets qui le caractérisent. Les termes non canoniques sont les termes obtenu appliquant une opération aux termes canoniques et une fois calculés donnent un terme canonique. Les termes sont vu comme des programmes et deux termes sont égaux quand leur calcul donne le même résultat, c'est à dire le même terme canonique. On introduit la notion de comportement principal, qui est bien adapté à la représentation des termes canoniques. On introduit aussi la notion de comportement séparable, qui nous donne un outil pour définir les fonctions de manière simple.On représente les nombres naturelles, les listes, les records, les fonctions dépendantes, les couples et on discutes les records dépendantes.On se focalise après sur la Théorie de Martin-Lof pour proposer une représentation de certaines types de base et constructions. ; This thesis proposes a representation of the notion of type, with a particular interest on dependent types, in Ludics.Ludics is a theory introduced by Girard cite{LocSol}. It comes from a fine analysis of the multiplicative, additive fragment of polarized Linear Logic (MALL_p). One of its aim is to reconstruct logic from the notion of interaction. A type is a class of objects that behave in the same way with respect to other objects.The notion of type ...