Fixpoints of types in linear logic from a Curry-Howard-Lambek perspective

Points fixes de types en logique linéaire d'un point de vue Curry-Howard-Lambek Cette thèse porte sur l'étude d'une extension de la logique linéaire propositionnelle avec des points fixes de type dans une perspective Curry-Howard-Lambek. La logique linéaire à points fixes de types, appelée \mu LL, nous permet d'avoir des preuves inductives et coinductives. Nous développons une sémantique catégorielle de \mu LL basée sur les catégories de Seely et sur des foncteurs "strong" agissant sur elles. Ensuite, nous introduisons et étudions \mu LLP comme une extension de la logique linéaire polarisée, avec plus petit et plus grand points fixes. Profitant des règles structurelles implicites de \mu LLP , nous introduisons une syntaxe de terme pour ce langage, dans l'esprit du \lambda-calcul classique et du système L. Nous équipons ce système logiqued’une sémantique de réduction déterministe ainsi que d’une sémantique catégorielle. Nous examinons toujours notre sémantique catégorielle avec des cas concrets tels que la catégorie des ensembles et des relations, la catégorie des ensembles munis d'une notion de totalité (espaces de totalité non uniformes) et des relations qui préservent a totalité, et les espaces de cohérence avec totalité. Dans le cas de \mu LLP, nous prouvons un résultat d'adéquation pour \mu LLP entre sa sémantique opérationnelle et dénotationnelle, dont nous dérivons une propriété de normalisation grâce aux propriétés de l'interprétation de la totalité. Nous étudierons également les preuves non bien fondées en logique linéaire, que l'on peut voir comme une extension des preuves inductives, d'un point de vue sémantique dénotationnelle en faisant une relation entre condition de validité des preuves non bien fondées et interprétation de la totalité. Enfin, nous fournirons un modèle catégoriel pour les exponentielles codées à l'aide de l'opérateur de point fixe.