EXECUTION ET PROGRAMMES / MARCO PEDICINI ; SOUS LA DIR. DE JEAN-YVES GIRARD

Date :

Editeur / Publisher : [S.l.] : [s.n.] , 1999

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : anglais / English

Girard, Jean-Yves (1947-....) (Directeur de thèse / thesis advisor)

Université Paris Diderot - Paris 7 (1970-2019) (Organisme de soutenance / degree-grantor)

Résumé / Abstract : LE SUJET DE CETTE THESE EST L'ETUDE DES ASPECTS OPERATIONNELS DU LAMBDA CALCUL ET DE LA LOGIQUE LINEAIRE A L'AIDE DE LA GEOMETRIE DE L'INTERACTION, UN MODELE MATHEMATIQUE DE L'EXECUTION DES PROGRAMMES, INTRODUIT PAR JEAN-YVES GIRARD EN 1987-88. CETTE THESE SE COMPOSE DE QUATRE CHAPITRES DISTINCTS ET INDEPENDANTS : - CHAPITRE 1 : LOGIQUE LINEAIRE ET LAMBDA CALCUL UN RESULTAT CLASSIQUE DU LAMBDA CALCUL, LE LEMME DU BOHM-OUT, EST ETENDU AU CAS DES RESEAUX PURS. - CHAPITRE 2 : GEOMETRIE DE L'INTERACTION ET IMPLEMENTATION. LA REDUCTION VIRTUELLE ORIENTEE EST INTRODUITE : IL S'AGIT D'UNE EXTENSION DE LA NOTION DE REDUCTION VIRTUELLE INTRODUITE PAR DANOS ET REGNIER. POUR LA REDUCTION VIRTUELLE ORIENTEE, UNE NOUVELLE STRATEGIE, DITE DE COMBUSTION, EST ETUDIEE. - CHAPITRE 3 : GEOMETRIE DE L'INTERACTION ET COMPLEXITE LE LIEN ENTRE LOGIQUE ET COMPLEXITE EST ETUDIE, A TRAVERS LA LOGIQUE LINEAIRE ELEMENTAIRE (ELL) : DANS LES MODELES DE L'EXECUTION DE CE SYSTEME, LA COMPLEXITE DES EXECUTIONS EST BORNEE PAR CELLE DE L'ELIMINATION DES COUPURES DE ELL. - CHAPITRE 4 : GEOMETRIE DE L'INTERACTION ET CATEGORIES. DANS LE BUT DE COMPRENDRE LA GEOMETRIE DE L'INTERACTION DANS LE CADRE DE LA THEORIE DES CATEGORIES, ON INTRODUIT UNE NOTION DE CONVERGENCE SUR DES CATEGORIES SEMANTIQUES, LES CATEGORIES PARTIELLEMENT ADDITIVES INTRODUITES PAR MANES-ARBIB.