de carvalho-these

UNIVERSITÉ DE LA MÉDITERRANÉE Aix Marseille IIÉCOLE DOCTORALE DE MATHÉMATIQUES ET INFORMATIQUE E.D. 184THÈSEprésentée pour obtenir le grade deD  ’U´   M´ ´Spécialité : MathématiquesparDaniel DE CARVALHOTitre :Sémantiques de la logique linéaireet temps de calculsoutenue publiquement le 4 septembre 2007JURYM. Patrick BAILLOTM. Pierre Louis CURIENM. Thomas EHRHARDM. Martin HYLAND RapporteurM. François LAMARCHEM. Kazushige TERUIM. Lorenzo TORTORA DE FALCO RapporteurKateTable des matièresRemerciements 9Introduction 11Préliminaires 151 Préliminaires catégoriques 171.1 Catégories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 171.2 enrichies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 202 La logique linéaire 232.1 Les formules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 232.1.1 Le fragment intuitionniste . . . . . . . . . . . . . . . . . . . . . . . . . . . 232.1.2 La logique linéaire classique . . . . . . . . . . . . . . . . . . . . . . . . . . 232.2 Le calcul des séquents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 242.2.1 Le fragment intuitionniste . . . . . . . . . . . . . . . . . . . . . . . . . . . 242.2.2 La logique linéaire classique . . . . . . . . . . . . . . . . . . . . . . . . . . 242.3 Les réseaux . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 252.3.1 ...