Le sujet de cette thèse est l’étude de l’encodage des références et de la concurrence dans la Logique Linéaire. Notre motivation est de montrer que la Logique Linéaire est capable d’encoder des effets de bords, et pourrait ainsi servir comme une cible de compilation pour des langages fonctionnels qui soit à la fois viable, formalisée et largement étudiée. La notion clé développée dans cette thèse est celle de zone de routage. C’est une famille de réseaux de preuve qui correspond à un fragment de la logique linéaire différentielle, et permet d’implémenter différentes primitives de communication. Nous les définissons et étudions leur théorie. Nous illustrons ensuite leur expressivité en traduisant un λ-calcul avec concurrence, références et réplication dans un fragment des réseaux différentiels. Pour ce faire, nous introduisons un langage semblable au λ-calcul concurrent d’Amadio, mais avec des substitutions explicites à la fois pour les variables et pour les références. Nous munissons ce langage d’un système de types et d’effets, et prouvons la normalisation forte des termes bien typés avec une technique qui combine la réductibilité et une nouvelle technique interactive. Ce langage nous permet de prouver un théorème de simulation, et un théorème d’adéquation pour la traduction proposée. / The topic of this thesis is the study of the encoding of references andconcurrency in Linear Logic. Our perspective is to demonstrate the capabilityof Linear Logic to encode side-effects to make it a viable, formalized and wellstudied compilation target for functional languages in the future. The keynotion we develop is that of routing areas: a family of proof nets whichcorrespond to a fragment of differential linear logic and which implementscommunication primitives. We develop routing areas as a parametrizable deviceand study their theory. We then illustrate their expressivity by translating aconcurrent λ-calculus featuring concurrency, references and replication to afragment of differential nets. To this purpose, we introduce a language akin toAmadio’s concurrent λ-calculus, but with explicit substitutions for bothvariables and references. We endow this language with a type and effect systemand we prove termination of well-typed terms by a mix of reducibility and anew interactive technique. This intermediate language allows us to prove asimulation and an adequacy theorem for the translation
| Identifer | oai:union.ndltd.org:theses.fr/2018USPCC190 |
| Date | 25 September 2018 |
| Creators | Hamdaoui, Yann |
| Contributors | Sorbonne Paris Cité, Faggian, Claudia, Valiron, Benoit |
| Source Sets | Dépôt national des thèses électroniques françaises |
| Language | English |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation, Text, Collection |
Page generated in 0.0021 seconds