Linearity and beyond in demotational semantics

Dans cette these, nous proposons une exploration de la notion de linearite, dans plusieurs de ses aspects. Par le terme "linearite" nous entendons tous les concepts plus au moins lies aux idees qui sont a l'origine de la Logique Lineaire de Girard. Plus precisement, dans cette these nous presentons le langage S1PCF, un langage de programmation semantiquement lineaire. S1PCF est denotationellement lineaire car il est concu comme la contrepartie syntaxique des Fonctions Lineaires Stables des Espaces Coherents. Nous etudions des modeles denotationnels de S1PCF, nous montrons un resultat de full abstraction et nous discutons des extensions de ce langage. Nous presentons un modele syntaxique de S1PCF en donnant un codage fidele de ce langage de programmation dans un langage de processus appele linProc. Nous poursuivons notre etude de la linearite dans les langages de processus, en proposant la Ludique de Girard comme un outil mathematique abstrait pour etudier des proprietes importantes des processus, comme la liveness ou l'absence de deadlock. Nous donnons un modele semantique du pi-calcul lineaire dans une version modifiee de la Ludique concue pour valider la regle du Mix. Enfin, nous allons au-dela de la linearite en donnant une caracterisation logique de la stabilite, en utilisant les types intersections. Nous definissons deux systemes d'assignation de type pour le lambda-calcul qui sont parametriques sur une relation de coherence entre types. Nous prouvons que ces systemes donnent une caracterisation logique de deux classes interessantes de modeles du lambda-calcul.