Programmer, calculer et raisonner avec les réseaux de la Logique Linéaire

La premiere partie propose divers systemes de reseaux d'interaction (calcul par reecriture muni d'une reduction atomique, locale et parallele) qui simulent l'execution des preuves de la logique lineaire (considerees comme des programmes). Les differents fragments de cette logique sont abordes, on y ajoute aussi une recursion pour atteindre l'expressivite des langages de programmation usuels. Ce procede de simulation permet d'executer certains langages a l'aide d'une petite machine d'execution multi-processeurs. Il s'appuie sur des representations localisees de boites issues des reseaux de preuve ; certaines utilisent avantageusement un canal de controle pour ne rien perdre de la structure des preuves representees. La deuxieme partie s'articule autour de la logique lineaire differentielle et de ses ressources a usage unique. On la munit d'une super-promotion, qui se distingue notamment d'une promotion ordinaire parce qu'elle preserve la symetrie originelle de ce formalisme. C'est la pendante cote logique de la replication qu'on trouve parfois dans les algebres de processus. On arrive a isoler l'un de ses composants plus primitifs, le co-enfouissement, responsable de leur dynamique incontrolee (pour l'instant). Cette construction peut etre exprimee dans la syntaxe du λ-calcul avec ressources ou dans un systeme de reseaux. La sequentialisation de ces derniers requiert une presentation originale de la logique, fondee sur un calcul de structures, et qui a potentiellement d'autres interets. Il est aussi question de realisabilite pour les systemes differentiels et de semantique relationnelle pour les divers reseaux presentes.