Vers une ludique différentielle / Stéphane Zimmermann ; sous la direction de Thomas Ehrhard et Pierre-Louis Curien

Date :

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

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Logique mathématique

Lambda-calcul

Calcul différentiel

Ehrhard, Thomas (1961-... ; mathématicien) (Directeur de thèse / thesis advisor)

Curien, Pierre-Louis (1953-....) (Directeur de thèse / thesis advisor)

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

Relation : Vers une ludique différentielle / Stéphane Zimmermann ; sous la direction de Thomas Ehrhard et Pierre-Louis Curien / Lille : Atelier national de reproduction des thèses , 2013

Résumé / Abstract : Cette thèse se place dans le cadre de l'étude de la logique linéaire. La ludique est l'examen des preuves de la logique linéaire selon leur comportement au lieu de leur structure. Ce travail a déjà été fait pour la partie affine de la logique linéaire et diverses extensions ont été proposées pour rajouter des répétitions. Le but de cette thèse est de voir si la logique linéaire différentielle permet de résoudre les problèmes liés aux répétitions. Dans une premiere partie nous étudions le calcul des séquents de la logique linéaire différentielle pour lequel nous prouvons une propriété de focalisation. Cette preuve est obtenue de deux manières différentes par encodage des preuves dans une variante différentielle de la logique tensorielle de Melliès. Dans une seconde partie, nous étudions un langage de termes obtenu à partir des preuves focalisées. Nous donnons deux système de types pour ce langage, un différentiel et un total, ainsi qu'un modèle de réalisabilité pour le second système.

Résumé / Abstract : This thesis is a contribution to the study of linear logic and of ludics in particular. Ludics is a what to examine proofs of linear logic through their behavior. This has already been done for the affine part of linear logic and various extensions have been proposed to deal with the repetitions. The purpose of this thesis is to see if the differential linea logic can provide a good way to handle these repetitions. In the first part we study the sequent calculus for differential linear logic and we show a focalisation property for it. The property is obtained in two ways, using different encodings in a differential variant of Melliès' tensor logic. In the second part, we study the term syntax obtained from focalised proofs. We give two typin systems for this langage, one differential and one without failures, and we give a realizability model for the second system.