Differential nets experiments and reduction
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
Supervised by Prof. Tortora de Falco (Universita Roma Tre) and Prof. Ehrhard (Université Paris Diderot - Paris 7), my thesis research is focused mainly on two topics: 1) linear logic, especially in its differential version, where my principal contributions are the introduction of a non-inductive (i. E. "more geometric") syntax for multiplicative and exponential (differential) linear logic nets and the study of the relationship between experiments of relational semantics and Taylor expansion of a linear logic net, which leads to simplify the proof of the injectivity of relational semantics for acyclic and connected nets; 2) the call-by-value lambda calculus studied from the point of view of linear logic, where my principal contributions are the study of the call-by-value beta-reduction (and some abstract machines implementing it) and the definition of an extension of the call-by-value beta-reduction which is induced by the "boring" Girard's translation of lambda-terms into multiplicative and exponential linear logic nets.
Abstract FR:
Sous la direction de M. Tortora de Falco (Université Roma Tre) et M. Ehrhard (Université Paris Diderot - Paris 7), mes recherches de thèse portent principalement sur deux thèmes : 1) la logique linéaire, notamment sa version différentielle, où mes contributions principales sont l'introduction d'une syntaxe non-inductive (c'est-à-dire « plus géométrique ») pour les réseaux de la logique linéaire (différentielle) multiplicative et exponentielle et l'étude du lien entre expériences de la sémantique relationnelle et développement de Taylor d'un réseau de la logique linéaire, ce qui mène a une simplification de la démonstration de l'injectivité de la sémantique relationnelle dans le cas des réseaux acycliques et connexes ; 2) le lambda-calcul par valeur étudié du point de vue de la logique linéaire, où mes principales contributions sont l'étude de la bêta-réduction par valeur (et des certaines machines abstraites qui l'implémentent) et la définition d'une extension de la bêta-réduction par valeur induite par la traduction « ennuyeuse » de Girard des lambda-termes dans les réseaux de la logique linéaire multiplicative et exponentielle.