Géométrie de l'interaction et réseaux différentiels
Institution:
Aix-Marseille 2Disciplines:
Directors:
Abstract EN:
In this dissertation, we study a non denotational semantic of proofs, or programs thanks to the Curry-Howard correspondances, the Geometry of Interaction. It consists in an algebraic characterization of paths preserved by cut-elimination. It relies on a presentation of proofs as some kinds of graphs from which we get a bnotion of paths. In the current work, we focus on the presentation given by interaction nets. In a first step, we give a completely explicit presentation of those nets. In a second step, we give definitions and properties in order to definie a Geometry of Interaction. We analyse the associated semantics for an infinite family of lambda-terms. At last, we introduce the framework of differential nets, an extension of linear logic, and build a Geometry of Interaction for them.
Abstract FR:
Dans cette thèse, nous nous intéressons à l'étude d'une sémantique non dénotationelle des preuves, ou programmes grâce à la correspondance Curry-Howard, la Géométrie de l'Interaction. Celle-ci consiste en une caractérisation algébrique des chemins préservés par élimination des coupures. Elle repose ainsi sur une présentation des preuves comme des graphes auxquels est associée une notion de chemins. Dans cette thèse, nous nous somme focalisés sur la présentation des données par les réseaux d'interaction. Dans un premier temps, nous présentons une définition complètement explicite de ces réseaux. Dans un second temps, nous présentons les définitions et propriétés en ue de définir une Géométrie de l'Interaction. Nous analysons notamment celle-ci pour une famille infini de lambda-termes. Finalement, nous nous plaçons dans le cadre des réseaux différentiels, extension de la logique linéaire, et construisons une Géométrie de l'Interaction de ceux-ci.