Abstract FR:

L'analyse de l'interpretation des regles structurelles, dans le cadre d'une semantique coherente de la logique lineaire, donne lieu a une caracterisation categorique de la structure des espaces coherents associes aux formules exponentielles. La structure la plus generale est celle de precomonoide, on retrouve les solutions deja connues dans la litterature comme cas particuliers. Parmi ces dernieres, la structure d'espace de correlation a ete utilisee par j-y girard dans la perspective d'une constructivisation de la logique classique: les espaces de correlations constituent une semantique denotationnelle du calcul des sequents lc. Les structures plus generale peuvent etre utilisees pour l'interpretation des preuves classiques formalisees dans un calcul lcg, plus contraint que lc. D'autre part, une extension au second ordre de lc et de sa semantique denotationnelle est realisee, en utilisant la theorie categorique des limites filtrantes. Enfin, nous exhibons un contre-exemple a la conjecture de completude enoncee pour la semantique denotationnelle de lc