Keywords: logique linéaire, sémantique, concurrence, références, parallélisme, réseaux de preuve, programmation fonctionnelle 2 Concurrency, References and Linear Logic linear logic, semantics, concurrency, references, parallelism, proof nets, functional programming

Concurrence, Références et Logique Linéaire Résumé 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.

ou gérerons notre narco-empire en Colombie, comme promis, Patròn. Gabriel, encyclopédie vivante d'oeuvres de science-fiction et de jeux vidéos, merci pour tes lumières sur OCaml et la programmation en général. Pierre, grimpeur de son état, merci pour tes calembours intempestifs et surtout d'avoir téléchargé l'intégralité de ncatlab dans ton cortex, ce qui s'est révélé très pratique pour tes cobureaux. Léo, merci pour rien. Entre les pauses thés, la dénigration systématique des Danois, de LaTeX, de la blockchain et du monde en général, j'apprécie bien trop ta compagnie pour avoir eu la moindre minute de travail à moi. Rémi, merci pour ton enthousiasme débordant et ta bienveillance, et pour l'exegèse collaborative de l'oeuvre de Girard. J'espère sincèremet que tu parviendra un jour à surmonter ton addiction à l'installateur Debian. Paulina, je te souhaite bien du courage pour la suite avec de tels énergumènes.

Dans l'étrange contrée de thésardie, je remercie le peuple autochtone qui a été aujourd'hui (presque) remplacé par une nouvelle génération: Etienne, PM et notre goût partagé pour les bons thés et les détournements scabreux, Gabriel S., Matthieu B., Pierre et Cyril pour leurs culture impressionante et dans des domaines parfois déroutants, Raphaëlle, Hadrien, Thibaut, et probablement une foultitude d'autres que ma mémoire défaillante n'est pas capable de se rappeler dans l'instant.

Je remercie aussi la nouvelle génération dont la compagnie aura été tout autant agréable: l'équipe gâteau, Victor et Cédric dirigés par le Général de Brigade Zeinab, pour votre gestion efficace de cette cérémonie et votre créativité sans limite dans les annoncements. Merci à Théo, Antoine, Léonard, Nicolas, Tommaso, Jules, Axel et les autres.

Vient le tour de mes autres amis, que je coremercie plutôt que remercie, au sens où j'aurais probablement pu finir ma thèse en 6 mois s'ils n'avaient pas été là. Mais ces 6 mois auraient été bien ternes et ennuyeux.

Les irréductibles de l'Essonne pour commencer, Geoffroy, Thib, Fabze, Jerem, Adeline et Rémy, dont certains m'ont supporté depuis si longtemps que j'ai arrêté de compter. Je pense que j'ai tellement de remerciements à vous faire qu'il me faudrait probablement écrire une seconde thèse pour qu'ils puissent y tenir. Ne changez rien.

Merci à Marianne, de m'avoir soutenu et encouragé, et de toujours avoir prêté une oreille à mes problèmes. Merci à Julie, de m'avoir supporté, voire porté parfois, et d'avoir été aussi présente pour moi. Vous avez été indispensables.

Merci à Quentin, que j'ai traîné dans les bas-fonds parisiens, et qui a toujours représenté avec dignité le clan familial.

Les GGs ensuite, pour avoir partagé l'antre du bonheur pendant presque un an. C'est dans cette ambiance d'émulation intellectuelle intense que j'ai établi ma toute première équation mathématique : "deux fois plus de cours = deux fois plus de temps libre". Gerblé, mon GG attitré et compère de toujours, homme-cheval-poisson, avec qui j'ai traversé des déserts de servitude et des champs de soleil. T,tjb. No12, co-anniversereux et déclaré meilleur rampeur d'anniversaires 2016, dit le Jawad de Strasbourg-Saint-Denis et adoré de tous ses voisins, merci de m'avoir accueilli comme je suis d'innombrable fois et pour ces diverses projections cinématographiques de qualité. Tu es une source d'inspiration inépuisable pour l'ensemble d'entre nous. Pie XII, vénérable catholique et milliardaire, grand gardien de la feuille de présence, tu m'as appris qu'il ne faut jamais cesser de se remettre en question dans la vie, et en particulier se demander: qui suis-je ? (rires). Jules, the defusable man, jamais aussi splendide qu'échoué en peignoir sur le canapé, merci d'avoir écouté mes élucubrations mathématiques et informatiques avec grand intérêt. Puis l'équipée de Bois-Colombes et la nébuleuse qui gravite autour. La Meum's, depuis cette aventure du Dekmantel au tout début de ma thèse, on ne s'est plus vraiment quittés. Grand maître des afters squares et du n'importe quoi en général, srab d'escalade et soudé dans l'adversité capillaire, merci pour tout. Poupours, douce comme un ageneau (sic), Agatha-chan rockstar et artiste martial à ses heures perdues, la Mache, le meilleur protostagiaire que j'ai eu l'occasion de former, la Valj ou la nonchalance, Goldyboy le champion de course de brouettes, la Franche, Amiral de la Narine et Capitaine de chaloupe inégalé dans toute la mer d'Iroise, Eliott et sa fine connaissance du rap et des belles tapisseries, la couls, la Glache, Coralie, Sarah, Bap, la Basse, la Masse, et tous les autres que j'ai pu oublier.

Merci aux Michels, Lulu d'am a.k.a Lucifer, petite Margot, Léa mon sujet préféré de toute la Rabzouzie, Tangouze no limit, Fedi la plus belle des princesses Niglo, Fourmarie, femme de goût aussi bien vestimentairement que gastronomiquement parlant, Beber, Marie, Hélo, Blondie car qu'est-ce qu'un Picon sans Ducon, Tinmar, Felix, Thibax, et tous les autres pour avoir égayé ces années de vos picons chouffe. Merci d'être vous.

Merci aux faisands et assimilés, nouveaux ou anciens, Jonath, Jess, Jerem & Jerem, Nico, Hélène, Tom, Marion, Jim, Romain, Ben, Baddri, Eliot, Mike, Chloé, Léo, Paula, Adriana, Morgane, Jaimito, Clara, Charlie et tous les autres. Merci pour votre bonne humeur et vos talens musicaux. Je suis toujours ressorti ressourcé de votre belle maison.

Merci aux Centraliens, Doc d'amoume, Baza l'affreux, Foox le fooxien, La Croute, Sancho, Manus, Denver, Passpass, Gob, Billou, Babass, et tous les autres que je n'ai pas la place de citer, pour ces repas odieux au japonais.

Enfin, merci aux Originaux, Anti, Adri, Mariche, Eugé, Ben, Louis et toutes les autres belles personnes qui gravitent autour de vous pour avoir rendue un peu plus douce ma période de rédaction et de préparation de soutenance. Paradoxalement, le FOMO qui a découlé de l'Origine s'est transformée en un puissant moteur pour la rédaction de mon manuscrit. [START_REF] Accattoli | The structural λ-calculus[END_REF] The concurrent λ-calculus with explicit substitutions λ cES 4.

Introduction

Computer science is no more about computers than astronomy is about telescopes, biology is about microscopes or chemistry is about beakers and test tubes.

Michael R. Fellow, Ian Parberry

Computations have existed long before computers and computer science. Babylonians had, for example, precise descriptions of algorithms to compute the solutions to various geometric problems more than one millennium before the beginning of formal algebra. What is maybe less intuitive, partly because of the English conflation of the word computer in "computer science" with modern electronic computers, is that computer science was also born before computers as we know them today, roughly in the 1930's. Alan Turing may be considered as the father of modern computer science. He proposed the concept of a Turing machine [START_REF] Mathison | On computable numbers, with an application to the entscheidungsproblem[END_REF], a mathematical model that answers the question "What is a computation ?" and the not less fundamental question of what can be computed, and what can not be. While his work is a cornerstone of computer science, mathematicians -or rather computer scientists -have found that Turing machines are very far from being the only answer to this question. On the contrary, an astonishing number of different systems are able to express computations in different forms, from λ-calculus to graph rewriting systems. A lot of these models have exactly the same computing power: they can do as much as a Turing machine, and no more, that is they are Turing-complete. The Church-Turing thesis precisely claims that the notion of computation is captured by Turing machines. This is illustrated nowadays by the large zoology of general purpose programming languages available to developers which are all capable of expressing the same algorithms, but not in the same way, not with the same performance, or not as easily, depending on the task to be performed and the language considered.

The Curry-Howard Isomorphism In the 50s and 80s, Curry and Howard made the fundamental observation that there is a deep connection between mathematical proofs and computer programs [START_REF] William | The formulae-as-types notion of construction[END_REF]. Basically, the mathematical activity of proving a theorem is analogous to the one of programming. Programmers split their programs into small independent and reusable blocks, called functions. They take arguments, their input, and return a result, the output. One can take for example a function that takes a list of textual data as an argument and returns the same list but sorted alphabetically. Then, whenever needed, this function is applied to given arguments and produces the desired output. This function may then be used in diverse softwares, such as the contacts manager of a smartphone or an online dictionary. The implementation is independent from the usage: all this function has to know is the list it takes as an argument to provide a result. Mathematicians proceed exactly in the same way. Due to the complexity and the breadth of the mathematical knowledge, results are often broken down into multiple pieces: lemmas, theorems, definitions, propositions, properties, etc.. They share the same purpose and characteristics as functions in programs. Application then corresponds to a cut, or its more intuitive emanation modus ponens: from a proof of A =⇒ B -or rather, in our new interpretation, a function from A to B -and a proof of A (a data of type A), one deduces B (one gets a data of type B by applying the function to the argument). This intuition can be framed in a very precise framework, both on the logic side and the programming side: proofs in propositional intuitionistic logic are in correspondence with programs of the simply typed λ-calculus, associating the following objects [START_REF] William | The formulae-as-types notion of construction[END_REF]:

Logic

Programming Propositions Types Proofs Programs Cut-elimination Execution This realization has spawned a substantial corpus of research and results. People started to import concepts of logic inside computer science, and concepts of computer science inside logic. The fact that proofs carry a computational result led to program extraction, a technique that synthesizes a program from a proof, for example a program implementing an algorithm from the proof of its termination. Type theory has led to the development of proof assistants, giving an unified environment to write both a program, properties about this program, and proofs of these properties all in the same language. Girard [START_REF] Girard | Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur[END_REF] (and independently from a purely programming approach, Reynolds [START_REF] Reynolds | Towards a theory of type structure[END_REF]) extended the Curry-Howard isomorphism by introducing polymorphic λ-calculus System F, which corresponds to second order intuitionistic logic. System F is the foundation of many modern functional programming languages such as Haskell or OCaml. In general, the Curry-Howard isomorphism gave a totally new status to types in programs. From a simple tag addressed to the compiler specifying how generic binary data should be handled, as are types in C for example, they have become first class entities expressed in their own language, which are able to attach a logical specification to a piece of code, to drive optimization, static analysis, etc.

Linear Logic Girard introduced Linear Logic (LL) in his seminal paper [START_REF] Girard | Linear logic[END_REF]. The distinctive feature of LL is to be a resource-aware logic, which explains its success as a tool to study computational processes. Indeed, in LL, the usage of resources is controlled and explicit: using an hypothesis once is not the same as using it twice. The native language for LL proofs -or rather, programsare proof nets, a graph representation endowed with a local and asynchronous cut-elimination procedure. The fine-grained computations and the explicit management of resources in LL make it an expressive target to translate various computational primitives. Girard provided two translations of the λ-calculus to LL in its original paper, later clarified as respectively a call-by-value and call-by-name translation of the λ-calculus [START_REF] Maraist | Call-byname, call-by-value, call-by-need, and the linear lambda calculus[END_REF].

Parallelism An important feature of languages based on the λ-calculus, i.e. functional languages, is that they tend to expose the intrinsic parallelism of programs. This has been responsible in part for the dramatic increase in interest in functional languages and functional paradigms over the last years, which have percolated through mainstream programming languages: lambdas, closures, monads, algebraic effects, immutability, type inference, etc.. And for a very good reason: processor technology have bumped into physical limits that prevent any further increase in frequency or transistor density. To continue to improve performances, manufacturers resort to rather delivering more and more cores that all run in parallel on a single CPU. On a different scale, the development of cloud computing, coupled with a high internet speed, gives the possibility of performing computations on huge grids of thousands and thousands of processing units. This has caused a total paradigm shift in program development: to take advantage of this new speed up capability, classical imperative programs must often be totally rethought and rewritten. Indeed, mutability, encouraged in imperative programming, affect the whole state of the computer. There is no obvious way to automatically parallelize such programs written with the mental model that they would be executed sequentially and alone on a CPU. Even when one wants to write parallel programs in such languages, one must resort to specific and error prone mechanisms of synchronization to avoid data races and deadlocks. On the other hand, writing a program which assures the same functionality in a pure functional language forces, by design, to write code that is easily parallelizable. This property is shared by programs expressed in LL, thanks to the local and asynchronous graph-reduction of proof nets.

Concurrency and Effects Automatic parallelization is not the only challenge of modern programming. Either via the internet, or even on a single computer, today programs live in a concurrent world. They are exchanging information with other programs and in the same time competing for resources. Programming models must incorporate this dimension and offer primitives to perform and control this kind of interactions. While λ-calculus is a fundamental tool in the study and design of functional programming languages, mainstream programming languages are pervaded with features that enable productive development such as support for parallelism and concurrency, communication primitives, imperative references, etc. Most of them imply side-effects, which are challenging to model, to compose, and to reason about. Some effects, such as imperative references, are non commutative: the order of evaluation matters and may change the result of a computation. Together with parallelism, this induces a typical consequence of concurrency: non-determinism. Non determinism means that the same program, executed in the same environment, may give different and incompatible results. One simple example to illustrate this is a program composed of three threads in parallel accessing the same memory cell which holds an integer value. The first one tries to read the memory cell, the second one tries to write the value 0 in it, while the third one tries to write the value 1 in it. Depending on which of the writers is executed first, the reader may end up getting either 0 or 1.

Concurrent Curry-Howard The Curry-Howard isomorphism has been extended in many ways since its inception. As already mentioned, Girard extended it to second order with System F. Surprisingly, Curry-Howard is not restricted to constructive logics: Griffin discovered that Pierce's law, whose addition to intuitionistic logic gives back classical logic, corresponds to a construction known long before by Scheme programmers, call-with-current-continuation [START_REF] Griffin | A formulae-as-type notion of control[END_REF]. Krivine extends the computational interpretation to non-logical axioms, such as axioms of set theory in his classical realizability [START_REF] Krivine | Typed lambda-calculus in classical zermelo-fraenkel set theory[END_REF]. A long standing research direction has been the extension of Curry-Howard to concurrency, that is, find what could be the logical counter part of concurrent constructions of programming languages. Since the first similarities between processes calculi and proof nets have been observed, a lot of effort have been put in founding a concurrent version of the Curry-Howard isomorphism, but with limited success. To quote Damiano Mazza, "linear logic proofs are processes, but processes are far from being linear logic proofs and, what is more important, it is unclear at this time whether what is missing has any natural proof-theoretic counterpart" [START_REF] Mazza | The true concurrency of differential interaction nets[END_REF].

Goals and motivations

This thesis motivation is the belief that functional programming languages, and in particular LL -when seen as a programming language through the lens of the Curry-Howard isomorphism -are particularly amenable to parallelization and distributed computing. Moreover, the strong theoretical foundations of LL and the consequent research effort made since its inception also brings various extensions, semantics, abstract machines, complexity analysis techniques, implementation schemes, etc. Even when the settings does not exactly match the standard framework of LL, many ideas and notions are still usable or adaptable.

We think that the fine-grained and asynchronous dynamic of LL and its ability to express many computational paradigms make it a good candidate to serve as a common target for compiling languages, i.e. a backend. In this regard, one may consider LL and derived systems as "functional assembly languages". Various translations of calculi to LL have already been investigated. Yet, they are often limited to a very austere setting (pure λ-calculus), do not necessarily accommodate side effects or concern rather modeling languages than actual programming language (cf Section 1.3). Our goal is to go one step further by modeling a language featuring at the same time concurrency, references and replication in LL. Our long-term intent is to exploit the ability of nets to enable independent computations to be done in parallel without breaking the original operational semantics. Concurrency and references are challenging as they lead to non-determinism and non commutativity which are two phenomena alien to standard LL. The approach to translate a concurrent calculus in nets that we propose in Chapter 5 can be seen as a compilation from a global shared memory model to a local message passing one, in line with proof nets philosophy.

To do so, we introduce a net system that is able to express concurrent behaviors. We develop a key tool for implementing communication primitives in this net system, routing areas, which are flexible and compositional. We illustrate their use through the encoding of a concurrent λ-calculus in nets, but we believe that they may be used in various future translations.

We tried to give a picture of what this thesis is about. Let us briefly mention what it is not. While the language we use to illustrate our tools through the translation features side-effects, a type system, and a usual λ-calculus syntax, it does not come close to something a developer would use in a day-to-day job. It lacks fundamental practical features. But it contains core constructs of concurrency, references, and function calls. We believe it is a convincing proof of concept for the ideas we develop. We do not claim to propose something like a concurrent Curry-Howard isomorphism either. Our nets are not correct, and as such do not correspond to a clear notion of proof. The dynamics is not the same in the source language and in nets, as a reduction step in the source language may be reflected by either zero or several steps in nets. However, given our goals and motivations, we do not require a correspondence as tight as one would expect from a variant of the Curry-Howard isomorphism. What is important is rather the preservation of the operational semantics of the source language.

Context

Linear Logic The creation of LL by Girard in [START_REF] Girard | Linear logic[END_REF] is a foundational work for this thesis. The idea of proof nets as a graphical parallel representation for proofs is already present in [START_REF] Girard | Linear logic[END_REF], and developed in [START_REF] Girard | Proof-nets: The parallel syntax for proof-theory[END_REF][START_REF] Danos | The structure of multiplicatives[END_REF], the latter introducing the Danos-Regnier criterion discriminating correct nets. Ehrhard and Regnier introduced Differential Linear Logic in [START_REF] Ehrhard | Differential interaction nets[END_REF], from which we borrow some rules to handle non-determinism. In his thesis, Tranquilli studies the rewriting system of differential proof nets with exponential boxes [START_REF] Tranquilli | Nets between determinism and nondeterminism[END_REF].

Geometry of Interaction and applications Together with Linear Logic, Girard initiated a program named Geometry of Interaction (GoI), which aims at giving a syntax-free representation of algorithms as independent mathematical objects [START_REF] Girard | Towards a geometry of interaction[END_REF]. He gives an interpretation of proofs of linear logic as endomorphisms on an Hilbert space, and an operator on these endomorphisms, the execution formula, which corresponds to the process of cut-elimination. Although this seems to be far away from practical considerations, GoI was later understood in a more concrete manner, as being about interaction paths in proof nets [START_REF] Asperti | Paths in the lambdacalculus. three years of communications without understanding[END_REF]. This gave a very operational presentation of GoI, as a reversible abstract machine which runs by moving a token along a proof net. Mackie saw in GoI a promising and novel approach for compilation [START_REF] Mackie | Applications of the Geometry of Interaction to language implementation[END_REF]. Ghica also uses GoI to enable programming in a high level functional language for integrated circuits [START_REF] Ghica | Geometry of synthesis: a structured approach to vlsi design[END_REF][START_REF] Dan | Geometry of synthesis ii: From games to delay-insensitive circuits[END_REF][START_REF] Dan | Geometry of synthesis iii: resource management through type inference[END_REF][START_REF] Dan R Ghica | Geometry of synthesis iv: compiling affine recursion into static hardware[END_REF]. Ghica also demonstrates how, with GoI-style machine, it is trivial to split and distribute computations over multiple processing units [START_REF] Fredriksson | Seamless distributed computing from the geometry of interaction[END_REF]. In [START_REF] Schöpp | On interaction, continuations and defunctionalization[END_REF], Schöpp shows that execution through GoI-like interactive semantics corresponds to well known compiler transformations: CPS-translation and defunctionalization. In [START_REF] Dal Lago | Parallelism and synchronization in an infinitary context[END_REF], Dal Lago and al. introduce a multi-token version of the GoI abstract machine for PCF. Multi-tokens do not only enable massive parallelism, but enable the same machine to support both call-by-value and call-by-name depending on the translation of terms, while single token GoI seems to be irremediably call-by-name without extension (Mackie gives a single-token call-by-value GoI compilation for λ-calculus, by allowing jumps). In [START_REF] Muroya | The dynamic geometry of interaction machine: a call-by-need graph rewriter[END_REF], Ghica and Muroya present a mixed graph rewriting/token machine that achieve call-by-need evaluation. In [START_REF] Hoshino | Memoryful geometry of interaction: from coalgebraic components to algebraic effects[END_REF][START_REF] Muroya | Memoryful geometry of interaction ii: recursion and adequacy[END_REF], the authors use categorical constructions to automatically derive GoI machines for various algebraic effects, such as first-order references or non deterministic choice. While we do not give a GoI abstract machine for the nets used in this thesis, these works -and especially the ambition of extending [START_REF] Dal Lago | Parallelism and synchronization in an infinitary context[END_REF] to a richer source language -were a strong motivation for extending known translations in linear logic to new computational paradigms.

Interaction nets and parallelism

The research on interactions nets and parallel evaluation is strongly linked to proof nets and geometry of interaction, although it was somehow led in parallel. In [START_REF] Lafont | Interaction nets[END_REF], Lafont abstracts away the key features of proof nets from the particular setting of LL: what he get is the generic graph rewriting system of Interaction Nets (INs). INs share the same locality and asynchronicity properties as proof nets, which naturally leads to parallel implementation. In [START_REF] Sousa | Sequential and concurrent abstract machines for interaction nets[END_REF], Pinto gives a parallel abstract machine for interaction nets. In [START_REF] Jiresch | Towards a gpu-based implementation of interaction nets[END_REF], Jiresch proposes to exploit the massive parallelism of modern GPUs to execute interaction nets, while Kahl gives another parallel implementation in Haskell [START_REF] Kahl | A simple parallel implementation of interaction nets in haskell[END_REF]. In his thesis, Mazza studies the semantics of interaction nets and propose a non-deterministic variant, multiport interaction nets, able to encode concurrent calculi [START_REF] Mazza | Interaction nets : semantics and concurrent extensions[END_REF]. Dal Lago, Tanaka and Yoshimizu gives a GoI for multiport interaction nets in [START_REF] Lago | The geometry of concurrent interaction: Handling multiple ports by way of multiple tokens[END_REF].

Encoding of references and concurrency in proof nets A part of this thesis (Chapter 4 and Chapter 5) is dedicated to the translation of a concurrent calculus to nets. This illustrates the expressivity of routing areas and the nets system. Our work is built on a series of previous works. Girard provided two translations of the simply typed λ-calculus in its original paper [START_REF] Girard | Linear logic[END_REF], later clarified as respectively a call-by-value and call-by-name translation of the λ-calculus [START_REF] Maraist | Call-byname, call-by-value, call-by-need, and the linear lambda calculus[END_REF]. Other works have tackled the intricate question of modeling side-effects. State has been considered in a λ-calculus with references [START_REF] Tranquilli | Translating types and effects with state monads and linear logic[END_REF]. Another direction which has been explored is concurrency and non-determinism. In [START_REF] Honda | An exact correspondence between a typed pi-calculus and polarised proof-nets[END_REF], Honda and Laurent gives an exact correspondence between a typed π-calculus polarized proof nets. Ehrhard and Laurent then gives a translation of a fragment of πcalculus, and of acyclic solos (both without replication) in differential interaction nets [START_REF] Ehrhard | Interpreting a finitary pi-calculus in differential interaction nets[END_REF][START_REF] Ehrhard | Acyclic solos and differential interaction nets[END_REF]. In [START_REF] Mackie | Compiling process networks to interaction nets[END_REF], Mackie give an encoding of Kahn process networks to interaction nets. Kahn process networks are a model of computation based on a collection of sequential, deterministic processes that communicate by sending messages through unbounded channels.

Explicit substitutions A specially useful tool in the design of such abstract machines is the notion of explicit substitution, a refinement over β-reduction. The β-reduction of the λ-calculus is a meta-rule where substitution is defined inductively and performed all at once on the term. But its implementation is a whole different story: to avoid size explosion in presence of duplication, mechanisms such as sharing are usually deployed. Abstract machines implement various specific strategies that may either be representable in pure λ-calculus (call-by-value or call-by-name) or for which the syntax needs to be augmented with new objects (e.g. call-by-need or linear head reduction). The mismatch between β-reduction and actual implementations can make the proof of soundness for an evaluator or a compiler a highly nontrivial task. The heart of the theory of explicit substitutions, introduced in [START_REF] Abadi | Explicit substitutions[END_REF], is to give substitutions a first class status as objects of the syntax to better understand the dynamics and implementation of β-reduction. It consists in decomposing a substitution into explicit atomic steps. The main ingredient is to modify the β rule so that (λx.M )N reduces to M [N/x], where [N/x] is now part of the syntax. Additional reduction rules are then provided to propagate the substitution [N/x] to atoms.

Studied for the last thirty years [START_REF] Abadi | Explicit substitutions[END_REF][START_REF] Accattoli | Proof nets and the call-by-value λ-calculus[END_REF][START_REF] Accattoli | A nonstandard standardization theorem[END_REF][START_REF] Accattoli | leftmost-outermost) beta reduction is invariant, indeed[END_REF][START_REF] Accattoli | The structural λ-calculus[END_REF][START_REF] Gabbay | A new approach to abstract syntax involving binders[END_REF][START_REF] Kesner | A theory of explicit substitutions with safe and full composition[END_REF][START_REF] Lescanne | Explicit substitutions with de bruijn's levels[END_REF][START_REF] Høgsbro | Explicit cyclic substitutions[END_REF][START_REF] Sinot | Efficient reductions with director strings[END_REF], explicit substitution turns out to be a crucial device when transitioning from a formal higher-order calculus to a concrete implementation. It has been considered in the context of sharing of mutual recursive definitions [START_REF] Høgsbro | Explicit cyclic substitutions[END_REF], higher-order unification [START_REF] Lescanne | Explicit substitutions with de bruijn's levels[END_REF], algebraic data-types [START_REF] Gabbay | A new approach to abstract syntax involving binders[END_REF], efficient abstract machines [START_REF] Accattoli | Proof nets and the call-by-value λ-calculus[END_REF][START_REF] Sinot | Efficient reductions with director strings[END_REF], cost-model analysis [START_REF] Accattoli | leftmost-outermost) beta reduction is invariant, indeed[END_REF], etc. The use of explicit substitutions however comes at a price [START_REF] Kesner | A theory of explicit substitutions with safe and full composition[END_REF]. Calculi with such a feature are sensitive to the definition of reduction rules. If one is too liberal in how substitutions can be composed then a strongly normalizing λ-term may diverge in a calculus with explicit substitutions [START_REF] Mellies | Typed λ-calculi with explicit substitutions may not terminate[END_REF]. If one is too restrictive, confluence on metaterms is lost [START_REF] Curien | Confluence properties of weak and strong calculi of explicit substitutions[END_REF]. The challenge is to carefully design the language to implement desirable features without losing fundamental properties. Several solutions have been proposed to fix these defects [START_REF] Accattoli | The structural λ-calculus[END_REF][START_REF] Kesner | A theory of explicit substitutions with safe and full composition[END_REF] for explicit substitutions of term variables.

Related works

We discuss more in detail work that is closely related to this thesis and has similar objectives. As a matter of fact, our thesis builds on the following papers:

1. In [START_REF] Ehrhard | Interpreting a finitary pi-calculus in differential interaction nets[END_REF], Ehrhard and Laurent proposes a translation of a fragment of πcalculus in differential nets. The π-calculus is designed to be a model of concurrent processes. As such, it features non-determinism, and the authors show that a possible answer to the problem of encoding it in nets is to switch to differential linear logic. The limit of their work is that they interpret a π-calculus without sums nor replication. Correspondingly, they consider a promotion free version of differential nets. The authors introduce the notion of communication area, a device introduced to implement communication in nets. Communication areas are specific nets that enable communication between the processes (actually, their encoding as nets) that are plugged in it. In this thesis, we present and study a generalization: routing areas (Chapter 3). We discuss how routing areas extend communication areas in Section 3.5. Our approach allows the interpretation of a calculus with replication.

2. In [START_REF] Tranquilli | Translating types and effects with state monads and linear logic[END_REF], Tranquilli introduces an encoding of a λ-calculus with higher order references and a types and effects system to multiplicative exponential linear logic proof nets. He observes that the translation make explicit the independence of subprograms that operate on distinct references and allow their evaluation to potentially happen in parallel. In order to do so, he uses a monadic translation that allows to encode references inside a pure calculus, which is then translated through the usual call by value translation [START_REF] Maraist | Call-byname, call-by-value, call-by-need, and the linear lambda calculus[END_REF]. This is what Haskellers do, for example, when they use the state monad to emulate references. We build on the ideas of Tranquilli and propose the translation of a calculus with references and parallelism. However the combination of parallelism and references leads to non-determinism and possibly complex interleaved executions. It is not clear at all that this has a natural monadic encoding.

Let us clarify how we relate to these work.

• [START_REF] Tranquilli | Translating types and effects with state monads and linear logic[END_REF] interprets a deterministic sequential calculus with references inside proof nets. We present a translation of a concurrent and non-deterministic calculus.

• [START_REF] Ehrhard | Interpreting a finitary pi-calculus in differential interaction nets[END_REF] gives a translation from a replication-free π-calculus to differential nets, and introduces communication areas. We generalize communication areas and introduce routing areas. The calculus we propose features replication. More generally, while π-calculus is a fundamental tool adapted to the study of concurrent processes, it abstracts away too much detail of processes to resemble a programming language. It is rather a modelling tool. On the other hand, the calculus we use is based on the λ-calculus which, with few additions, is arguably a concrete programming language.

We use the concurrent calculus introduced by Amadio in [START_REF] Amadio | On stratified regions[END_REF] (actually the version described in [START_REF] Madet | Complexité Implicite de Lambda-Calculs Concurrents[END_REF]). It is a λ-calculus enriched with a parallel operator and references that can be read or modified through get and set operations. It is endowed with a types and effects system which ensures termination of well-typed terms. There is a lot of concurrent languages in the literature to chose from. This one is simple yet support core concurrent constructs.

Contributions

Routing areas In a concurrent imperative language, references are a means to exchange information between threads. In order to implement communication primitives in proof nets, we use and extend the concept of communication areas introduced in [START_REF] Ehrhard | Interpreting a finitary pi-calculus in differential interaction nets[END_REF]. A communication area is a particular proof net whose external interface, composed of wires, is split between an equal number of inputs and outputs. Inputs and outputs are grouped by pairs representing a plug on which other nets can be connected. They are simple yet elegant devices, whose role is similar to the one of a network switch which connects several agents. Connecting two communication areas yields a communication area again: this key feature enables their use as modular blocks that can be combined into complex assemblies. In this paper, we introduce routing areas, which allows a finer control on the wiring diagram. They are parametrized by a relation which specifies which inputs and outputs are connected. Extending our network analogy, communication areas are rather hubs: they simply broadcast every incoming message to any connected agent. On the other hand, routing areas are more like switches: they are able to choose selectively the recipients of messages depending on their origin. Routing areas are subject to atomic operations that decompose the operation of connecting communication areas. These operations also have pure algeabric counterparts directly on relations.

We show that routing areas are sufficient to actually describe all the normal forms of the fragment of proof nets composed solely of structural rules. The algebraic description of routing areas then provides a semantic for this fragment.

Computational content of nets We define and study a system of nets, derived from differential interaction nets, that is powerful enough to express concurrent primitives. However the translation of concurrent processes seems to unavoidably produce nets that do not respect the correctness criterion (as this was already the case in [START_REF] Ehrhard | Interpreting a finitary pi-calculus in differential interaction nets[END_REF]). Without a correctness criterion, the standard full-fledged reduction is neither confluent nor terminating. We observe however that imposing some constraints on this reduction allows to recover interesting properties. Notably, we argue that we may make up for abandoning global properties like termination by proving that particular nets are well-behaved: for example, we prove that if a net is weakly normalizing (without erasing reduction), then it is strongly normalizing. It suffices then to show that nets of interest are weakly normalizing to obtain strong normalization for them, even if general, there are non terminating nets. In the paper introducing differential nets [START_REF] Ehrhard | Differential interaction nets[END_REF], a foot notes precises that "[. . . ] incorrect nets might be interesting from a purely computational point of view". However, to our knowledge, the study of such systems in the literature is very limited.

Expressivity of routing areas : a translation of a concurrent λ-calculus to nets We illustrate the use of routing areas and our nets system by encoding the concurrent λ-calculus with explicit substitutions that we introduce. This translation combines the approach of [START_REF] Tranquilli | Translating types and effects with state monads and linear logic[END_REF] to accommodate references and [START_REF] Ehrhard | Interpreting a finitary pi-calculus in differential interaction nets[END_REF] to accommodate concurrency. The first one only considers state, and the second one a π-calculus without replication: we propose a translation of a language featuring higher-order references, concurrency and replication. We prove a simulation and an adequacy theorem.

Explicit substitutions for a concurrent λ-calculus In order to define and study the translation from a concurrent λ-calculus to nets, we introduce an intermediate language between the calculus and the nets. While the syntax and the structure of terms are still close to the original language, the dynamic is rather the one of nets, with a local and small-step reduction which distills the information through the whole term step by step. Our contributions are:

1. The definition of a system of explicit substitutions for a concurrent λ-calculus with references, both for variables and references.

The problem we address is the bidirectional property of assignment of references within a term. An assignment for a term variable in a redex only diffuses inward: in (λx.M )V , the assignment x → V only concerns the subterm M . Instead, a reference assignment set(r, V ) is potentially global: it concerns all the occurrences of the subterm get(r).

Our first contribution is to propose an explicit substitution mechanism to be able to express reference assignment step-wise, as for term-variables.

2. A proof of strong normalization for a typed fragment using a novel interactive property.

Akin to [START_REF] Amadio | On stratified regions[END_REF], the language we propose is typed and the type-system is enforcing strong-normalization. In the proof of [START_REF] Amadio | On stratified regions[END_REF] the infinitary structure of terms is restricted to top-level stores. In our setting, this would require infinite explicit substitutions which are subject to duplication, erasure, composition, etc.

Our proof only uses finite terms. It has a Game Semantics flavor which we find of interest on its own. Indeed, we use the idea of abstracting the context in which a subterm is executed as an opponent able to interact by sending and receiving explicit substitutions. Moreover, we believe that the finite, interactive technique we develop in this second contribution may be well-suited for different settings such as proof nets or other concurrent calculi.

Plan

Chapter 2 In Chapter 2, we introduce a graph programming language which is a fragment of differential nets. Our goal is to have a language which is both well-behaved and expressive enough to encode concurrent constructs. We do not impose any correctness criterion. We prove confluence of the reduction, and a conservation theorem, that is if we exclude erasing reduction steps (the one reducing to 0), then weakly normalizing nets are strongly normalizing. Section 2.1 defines of simple nets and nets. Section 2.2 defines the reduction rules on simple nets and show how to lift the reduction to formal sums of simple nets, that is nets. The next sections are dedicated to study various properties that the reduction satisfies. Section 2.3 shows confluence via the definition of a parallel reduction inspired by the proof of confluence of the λ-calculus. At last, Section 2.4 studies the zoology of terminating and non terminating nets. While the reduction we define is not terminating in general, we show that removing the erasing rule 0 → allows to show a property which imposes a strong condition on nets to be non terminating, limiting this possibility.

Chapter 3 In Chapter 3, we introduce routing areas, an extension of communication areas [START_REF] Ehrhard | Interpreting a finitary pi-calculus in differential interaction nets[END_REF]. In order to do so, various technical tools are introduced first. Section 3.1.1 introduces the notion of multirelation, a quantitative extension of relations between sets, which will be used to give an algebraic description of a routing area. Section 3.1.2 defines (co)contraction trees, which can be seen as generalized n-ary (co)contractions, and derives corresponding reduction rules. (Co)contraction trees will be the basic ingredients for building routing areas. Section 3.1.3 briefly reviews the correctness criterion which has been mentioned in Chapter 2. It will be used for various proofs of this chapter, as routing areas does satisfy the correctness criterion. Then, everything is in place to construct routing areas, which is done in Section 3.1.4. Section 3.2 describes constructions that allow to combine simple routing areas into more complex ones. We give two fundamental operations, juxtaposition and trace, and define the composition of routing areas from these two.

In Section 3.3, we observe that the interpretation of routing areas as communication devices extends to a larger class of nets, routing nets, which include routing areas. The necessity of recasting the notion of connection between endpoints in this setting leads us to give a formal treatment of path in Section 3.3.1. This tool allows to prove in Section 3.3.2 that the normal form of a routing net is a routing area. This provides a semantics that associates the multirelation describing its normal form to a routing nets. We study the properties of this semantics in Section 3.3.3, and show that it is closely related to paths. Chapter 4 In Chapter 4, we introduce the concurrent λ-calculus with explicit substitutions λ cES , with both substitutions for variable and references. The syntax and the operational semantics are given in Section 4.1. In Section 4.2, we introduce a type and effect system for λ cES , adapted from the one of λ C [START_REF] Amadio | On stratified regions[END_REF]. In presence of higher-order references, simple types does not suffice to entail strong normalization. On must use additional constraints: we use the idea of stratification, proposed by Boudol [START_REF] Boudol | Typing termination in a higher-order concurrent imperative language[END_REF]. It is nonetheless not trivial to extend the proof of strong normalization of well typed terms to the calculus with explicit substitutions. This is done in Section 4.3, where we use an interactive technique that is reminiscent of Game Semantics. At last, Section 4.4 focuses on the relation between λ cES and the language that inspired it, λ C . While λ cES should be thought of as a version of λ C with explicit substitutions, the latter is not a proper sublanguage of the former. We can however define an embedding of λ C in λ cES . We prove a simulation for this embedding in Section 4.4.2. In Section 4.4.3, we give an adequacy theorem, which is complementary to the simulation result. It states that the values than can be computed by a term of λ C and the ones that can be computed by its translation in λ cES are essentially the same.

Chapter 5 In Chapter 5, we illustrate the ideas we set up in previous chapter and propose an encoding of our concurrent calculus with explicit substitutions λ cES to nets. In Section 5.1, we give the definition of the translation. Section 5.1.1 reviews the monadic translation of [START_REF] Tranquilli | Translating types and effects with state monads and linear logic[END_REF] and explain how we adapt it to our setting. In Section 5.1.2, we detail how and why routing areas are used to design the translation. Then, Section 5.1.3 gives the encoding of λ cES terms in nets.

Section 5.2 is dedicated to the proof of simulation. It introduces some practical tools in Section 5.2.1, while the three following sections, Section 5.2.2, Section 5.2.3 and Section 5.2.4 treat the all the different cases.

Section 5.3 shows that the translation of a normal form is a strongly normalizing net. This is almost enough to show that the translation of any well-typed term is strongly normalizing, but we still miss an intermediate result to prove this claim (cf Section 5.5). We also show an adequacy property akin to the one between λ cES and λ C given in Chapter 4.

Chapter 2 Nets

In this chapter, we introduce a graph language which is a fragment of differential nets. Our goal is to define a fragment which is both well-behaved and expressive enough to encode concurrent constructs. By well-behaved, we mean that it satisfies a set of properties one would reasonably expect from a nets system. Concurrency, here in the form of the coexistence of both references and parallelism, leads to non-determinism. State is a non-commutative effect, as the order of evaluation matters and may change the result of a computation. On the other hand, parallelism allows multiple subprograms -in the form of threads -to be executed in an arbitrary order, whence the non-determinism. One simple example to illustrate this is a program composed of three threads in parallel accessing the same memory cell which holds an integer value. The first one tries to read the memory cell, the second one tries to write the value 0 in it, while the third one tries to write the value 1 in it. Depending on which of the writer is executed first, the reader may end up getting either 0 or 1. However, non-determinism seems to be outside of the realm of traditional LL: confluence enforces that the final outcome of a computation is unique and independent from the path of reduction. Fortunately, there is a well defined extension of LL, Differential LL, which supports non-determinism by operating not on terms but rather on formal sums of terms, where summands represent different and incompatible outcomes.

Correctness We will not require nets to verify the correctness criterion of Differential LL here: it turns out that the translation of concurrent calculi seems to naturally produce nets that do not respect the correctness criterion, which was already the case in [START_REF] Ehrhard | Interpreting a finitary pi-calculus in differential interaction nets[END_REF] for example (cf Section 2.6 for an extended discussion). A world without correctness is a wild world: in this setting, the full fledged reduction of (differential) LL is neither confluent (Figure 2.1) nor terminating ( Figure 2.3, Figure 2.2). The goal of this chapter is the definition and the study Overview Section 2.1 defines simple nets and nets. Section 2.2 defines the reduction rules on simple nets and shows how to lift the reduction to formal sums of simple nets, that is nets. The next sections are dedicated to study the various properties that the reduction satisfies. Section 2.3 shows confluence via the definition of a parallel reduction inspired by the proof of confluence of the λ-calculus. At last, Section 2.4 studies the zoology of terminating and non terminating nets. While the reduction we define is not terminating in general, we show that removing one problematic rule allows to show a property which imposes a strong condition on nets to be non-terminating, limiting this possibility.

Syntax

We can decompose our system into three layers (fragments):

Multiplicative The multiplicative fragment is composed of the conjunction ⊗ and the dual disjunction `. Here, the reduction produces the non-deterministic sum of the two outcomes. Cocontraction will be used as an internalized non-deterministic choice. While weakening weak A : !A → 1 erases a resource, the dual coweakening produces a resource ex nihilo: coweak A : 1 → !A. This is like a Pandora box: it can be duplicated or erased, but any attempt to consume it will turn the whole summand to 0, the neutral element of the non-deterministic sum. Coweakening is the neutral element of cocontraction.

Notation 2.1.1. We recall here some vocabulary of rewriting theory. An abstract rewriting system (ARS) is a pair (A, →) where A is a set and → ⊆ A×A is a binary relation on A, called a rewriting relation or a reduction. For an ARS (A, →), we write → + for the transitive closure and → * for the reflexive transitive closure. Let t ∈ A, a reduction sequence of t is a finite or infinite sequence (t 0 , t 1 , . . . , t i , . . .) i<N (where N ∈ N ∪ {∞}) of elements of A such that:

• t 0 = t • t i → t i+1
Let t ∈ A, we say that t is:

• a normal form if there exists no t ∈ A such that t → t .

• weakly normalizing if there exists a normal form n such that t → * n • strongly normalizing if there exists no infinite reduction sequence of t. Note that a strongly normalizing element is in particular weakly normalizing.

• confluent if for all u, u such that u * ← t → * u , there exists v such that u → * v * ← u two) free port is a free (resp. floating) wire.

A
5. A labelling of wires, which is a map from wires to the following fragment of LL: The set of simple nets is written S N .

F ::= 1 | ⊥ | F `F | F ⊗ F | !F | ?F . A
Definition 2.1.3. Depth Let S be a simple net. The depth of a port p in S is defined to be:

• 0 if p is a port of S • n + 1 if it is at depth n in a simple net associated to a box of S
Similarly, we define the depth of a cell or a wire as the depth of its ports. A port, cell or wire occurring at depth 0 is said to be at the surface.

Remark 2.1.4. As the simple nets are defined inductively, the depth of a port is a well defined positive integer.

The different kind of cells are illustrated in Table 2.1. We directly represent ! p cells as their associated simple net delimited by a rectangular shape. The well-founding condition ensure that such a representation is always possible. We impose that labels of wires connected to a cell respect the one given in Table 2.1, i.e that nets are well-typed.

We define the set of nets P N as the set of finite formal sums of simple nets, where each summand represents a different outcome in a non-deterministic context. Definition 2.1.5. Nets The set P N of nets is defined as formal sums of simple nets:

P N = { n i=1 S i | n ≥ 0, S i is a simple net}
The empty sum is denoted by 0.

Let us now give the reduction on nets.

Reduction

In this section, we define the rewriting system (P N , ⇒) on nets. To do so, we proceed in two stages:

1. We define (Section 2.2.1) a base reduction from simple nets to nets id est a relation → ⊆ S N × P N . We start from atomic rules describing how an elementary pattern may be rewritten , and then extend the reduction by allowing patterns to be reduced in an arbitrary context (Definition 2.2.1).

2. In Section 2.2.2, we lift → to reduction on nets, id est a relation ⇒ ⊆ P N × P N (Definition 2.2.3).

Base reduction →

We define the atomic rules as relations between S N and P N . By convention, we write them as one or several symbols over an arrow, such as er → for example. These are the base cases that describe how an atomic pattern can be rewritten in a simple net. In a non-deterministic context, it can produces several outcomes, hence the result is a net and not just a simple net. Atomic rules are illustrated in Table 2.2. They have the following general form:

where the interface of α and each β i are the same. The pattern on the left hand side of an atomic rule is called a reducible expression, or a redex. The right hand side of a rule is a reduct.

From these atomic rules, the reduction is then extended -still as a relation between S N and P N -by allowing redexes to be reduced inside an arbitrary context, that is a larger simple net that contains the redex. Reduction inside boxes is also permitted but only for a few rules (see Section 2.2.3).

We explain and detail the rules hereafter. • nd →: this is the non-deterministic reduction, which is the only one (beside the degenerate case of the 0) to produce an actual sum. When a dereliction tries to consume a resource composed of two resources packed through a cocontraction, two different outcome are produced. In the first summand, the left resource in consumed and the other is erased by a weakening. In the second summand, the inverse choise is made.

• ba →: the bialgebra rule express a commutation property between contraction and cocontraction. An operationnal interpretation is that gathering two resources non-deterministically through a cocontraction, and then copying this pack, is the same as first copying the resources individually and then packing the copy.

• s 1 →: this reduction expresses the interaction between coweakening and contraction. Coweakening is copied by a contraction just as a regular resource.

• s 2 →: this is the dual rule that expresses the interaction between weakening and cocontraction. It says that erasing a non-deterministic packing amount to individually erases each component.

• →: this rules says that coweakening is erased by a weakening, as a regular resource.

• 0 →: finally, this rules states than trying to consume a resource produced by a coweakening turns the whole simple net to 0.

Atomic rules only allow to reduce specific redexes. We want to be able to reduce these redexes whenever they appear in a larger simple net, by allowing the reduction to be performed up to an arbitrary context. We treat differently the extension of the reduction at surface and inside boxes, where only When one translates a type derivation of an intuitionistic system (take simplytyped λ-calculus for example) to nets, the explicit appearance of structural rules involves arbitrary choices. Indeed, there are many possbilities for the order of contractions of variables, the location of weakenings, etc. Not only these choices are irrelevant (the different representations behave the same way), but they are often not stable by reduction as the simulation of a reduction step in nets may end up with a different representation of the result. To avoid these issues, we quotient the nets by associativity and commutativity of (co)contraction (Table 2.3). The fact that this quotient is compatible with reduction confirms the irrelevance of these differences. The reduction (P N , ⇒) on nets is defined as the sum lifting of →.

We define a second notion of reduction on sums, which requires all summands that are not a normal form to perform a reduction step. This will prove useful when discussing properties about termination. Definition 2.2.4. Total reduction Let → a ⊆ S N × P N be a reduction from simple nets to nets. We define the rewriting system (P N , ⇒ tot a ) by: R ⇒ tot a n i T i if either S i is a normal form and

S i = T i , or S i → a T i .
The total reduction corresponding to → is (P N , ⇒ tot ).

About closed and surface reduction

Most of the rules are only allowed at the surface, meaning that they can not be performed inside boxes. This constraint is necessary to be able to encode weak reduction strategies of the λ-calculus. e → and er → are however allowed as they are harmless and do not correspond to any real computational step important inside λ-calculus. The closeness constraint, requiring boxes to not have auxiliary ports, fixes the non confluence of Figure 2.1 and the non-termination of Figure 2.3. But it does not change the fact that Figure 2.2 is looping, which seems harder to avoid without a correctness criterion. We will see in the section about termination that the closeness constraint still allows to recover termination properties weaker than strong normalization for some fragments, but sufficient for our purposes.

Confluence

In this section we prove that ⇒ is confluent (Theorem 2.3.5). We use the same approach as in the proof of confluence of λ-calculus: we define a parallel reduction ⇒ , which allows to perform an arbitrary number of steps in parallel. Parallel means that we can reduce several redexes at once, but only those that were originally present, as opposed to those that are created during the reduction. We have to treat separately reductions that are allowed anywhere, and those that are only allowed at the surface. This the reason why we first have to define a parallel reduction system only for the reductions allowed everywhere, (S N , → B ). From this, we extend this system to a reduction from S N to P N , → . We finally lift it to sums of net to define the complete parallel reduction (P N , ⇒ . Definition 2.3.1. → B Let (S N , → B ) be the reduction system on S N defined by the atomic rules that are allowed inside and outside boxes, that is → B = e → ∪ er →. We define the reduction system (S N , → B ) by:

• R→ B R • If R→ B S, then R→ B S. • If R→ B S, then • If R→ B T and S→ B U , then
We can now define the complete parallel reduction on simple nets.

Definition 2.3.2. →

We define the reduction → from simple nets to nets by:

• R → R • If R → S, then R → S • If R→ B S, then • If R → i T i and S → j U j , then

⇒ has the diamond property

Proof. The proof is performed by induction on the size of simple nets for → . The main point is that there is no actual critical pair. Thanks to the reflexivity of → , the diamond property is preserved when lifting the reduction to P N . Theorem 2.3.5 is an immediate corollary of Proposition 2.3.4. After confluence, we treat the issue of termination.

Theorem 2.3.5. Confluence The system (P N , ⇒) is confluent.

Normalizing and non-normalizing nets

Since we do not enforce any correctness criterion, we lose the guarantee of strong normalization (cf Figure 2.2 and Figure 2.3). Nonetheless some fragments of nets obtained by removing some reduction rules verify strong normalization. Others verify the (T 1 ) property (see Definition 2.4.3) which is not per se a termination property but which seriously limits the candidates for non-normalizing nets. This properties states that either a net is strongly normalizing, or it does not have a normal form at all. In this case, the mere existence of a normal form of a net is sufficient to deduce the finiteness of all reduction sequences of this net.

There is no hope for the full system (P N , ⇒) to satisfy (T 1 ), because the 0 → rule may erase a looping summand. See Figure 2.4 for a counter-example to (T 1 ) which is a slight modification of the looping example: at any moment, this net can either duplicate the looping pattern or reduce in one step to 0. However, Theorem 2.4.5 shows that removing the 0 → rule is sufficient to recover (T 1 ). The proof is carried out in three steps:

1. We first consider the subsystem of (P N , ⇒ tot ) composed only of reduction rules applied at the surface: (P N , ). We show that (P N , ) has the diamond property (Proposition 2.4.11), from which we deduce that it verifies (T 1 ) (Corollary 2.4.12).

2. We consider the remaining rules performed only inside boxes gathered in the subsystem (P N , ). We show that it is strongly normalizing (Proposition 2.4.10) and has a commutation property with (P N , ) (Proposition 2.4.7)

3. This commutation property allows us to show that (T 1 ) can be transported from (P N , ) to (P N , ∪ ), which is nothing but (P N , ⇒ tot ).

4. Finally, we show that the fact that (P N , ⇒ tot ) is (T 1 ) implies that (P N , ⇒) is (T 1 ).

Let us lay out the definitions of the reductions and the properties we use.

(P N , →) on nets verifies (T 1 ) if, whenever a net R is →- weakly normalizing, then R is →-strongly normalizing. Definition 2.4.4. Diamond A rewriting system (P N , →) is said to be diamond if whenever R 1 ← R → R 2 , then either R 1 = R 2 , or there exists T such that R 1 → T ← R 2 .
We can state the main theorem of this section: Theorem 2.4.5. (P N , ⇒) verifies (T 1 ).

The next proposition states the commutation property between (P N , ) and (P N , ). The proposition actually defines a transformation of reduction sequences: given a reduction composed of two consecutive blocks of respectively and reductions, we can produce a new reduction sequence with two new blocks in the reverse order ( followed by ). Moreover, if there is at least one step in the block, then the transformed sequence will also have at least one step in the block. This last point is fundamental for the lifting of the (T 1 ) property from to ∪ : it would not work anymore without it.

Remark 2.4.6. In principle, the different properties that we show about and should be proved on arbitrary sums of simple nets in regard to the definition of these reductions. This would however unnecessarily make for verbose proofs, which are already rather technical. This is why we will implicitly restrict ourselves in the proofs to the base case where the starting nets are simple nets (for example, S and R in the proof of Proposition 2.4.7). Thanks to the definition of the total reduction on sums, the base case is sufficient to extends all these properties to the total sum reduction.

S

We observe that the -redexes of R and S are in a one-to-one correspondence. Indeed, as reduction happens inside boxes, it can not create nor erase any -redex. We refer to the redex involved in S R (resp. R R ) as red (resp. red ), and to the rule applied as rule (resp. rule ). We consider different cases: We can do the same case analysis on R R as previously. We consider the case (d) separately. Once this statement is proved, we perform a second induction on the length of the reduction R → + R to obtain the desired result. Lemma 2.4.9 states that reduction steps preserve and reflect the fact of being a -normal form. As only acts on surface and inside boxes, the latter can neither create nor destruct redexes of the former.

Lemma 2.4.9. Neutrality of Let R * R . Then R is -normal if and only if R is.
Proof. Lemma 2.4.9

can not create nor erase -redexes.

We state the termination properties of the two reductions and . verifies (T 1 ) while is strongly normalizing.

Proposition 2.4.10. Strong normalization for is strongly normalizing.

Proof. Opening or deleting a box strictly decreases the total number of boxes in the net.

Proposition 2.4.11. Diamond for (P N , ) has the diamond property.

Proof. Proposition 2.4.11 This can be checked that the surfaceness and closeness constraints enforces the diamond property. The choice of taking the total lifting ⇒ tot is necessary for this proposition to be true, as well as the exclusion of the 0 rule, which would allow counter examples ("triangles") to exist.

Corollary 2.4.12. (P N , ) verifies (T 1 ).

Proof. Corollary 2.4.12 The surface reduction satisfies the diamond property, which precludes the existence of a term with both a normal form and an infinite reduction.

We can finally now prove Theorem 2.4.5. The fact that we prove is that

(P N , ∪ ) = (P N , ⇒ tot ) is (T 1 )
. The last step consist in showing that (P N , ⇒) and (P N , ⇒ tot ) have the same class of weakly and strongly terminating terms.

Proof. Theorem 2.4.5 We prove two auxiliary properties:

(a) →-weak normalization implies -weak normalization

Let R be →-weakly normalizing and R → * N a reduction to its normal form. By Proposition 2.4.8, we can write R * S * N . N being a →-normal form, it is also a -normal form, and by Lemma 2.4.9 so is S. R is thus -weakly normalizing.

(b) an infinite →-reduction gives an infinite -reduction

Let R be a net with an infinite →-reduction, written R → ∞. We will build by induction a reduction sequence

R = R 0 R 1 . . . R n . . . such that for any n, R n → ∞. Base case We just take R 0 = R Inductive case If R n R n → ∞, we take an infinite →-reduction starting from R n . If the first step is R n
S, then we take R n+1 = S. Otherwise, the first step is a step, and we take the maximal block of reductions starting from R n . By Proposition 2.4.10, this block must be finite and we can write R n * S S → ∞. By Proposition 2.4.7, we can swap the two blocks such that R n R * R * S → ∞, and we take R n+1 = R . From these two points, it follows that →-weak normalization implies →-strong normalization. If a net is →-weakly normalizing, then by (a) it is -weakly normalizing. By Corollary 2.4.12, it is also -strongly normalizing. But by (b) it must be also →-strongly normalizing.

Summary

In this chapter, we gave a definition of a non-deterministic nets system, a reduction on this system, and studied the properties of this reduction.

We first introduced simple nets that are defined as graph-like structures, whose cells -the analog of vertices -corresponds to rules of LL and wires to LL formulas. The rules we use are those of the multiplicative exponential fragment of LL, enriched with two rules coming from Differential LL, cocontraction and coweakening. The differential rules enable the expression of non-determinism. The non-determinism of the reduction is then accommodated by defining nets as formal sums of simple nets, where each summand represent a different outcome of the current computation. We then proceed to study some properties of this system.

We show that, although our system handles non-determinism, the introduction of formal sums allows to have confluence. In order to prove this, we constructed a parallel reduction ⇒ which we showed to be confluent in a very strong sense: it verifies a diamond property. Then we show that its transitive reflexive closure coincide with the one of the initially defined reduction on nets. This show the latter reduction is also confluent.

We then studied normalization in our system. Since we dropped the correctness criterion, all nets are not strongly normalizing, as illustrated by an example of a looping pattern (Figure 2.2). However we prove that in the fragment without the 0 → rule, nets that are not strongly normalizing are constrained: they can not reduce to any normal form. To prove this, we split the reduction in two: an inner reduction (which happens inside boxes) and a surface reduction. We studied these fragments independently, and how they interact. This allows us to prove that their union, which is the full reduction on nets (except the 0 → rule) verifies the property mentioned above.

Discussion

A distinctive feature of our system is that we do not require a correctness criterion. This has important consequences, as the traditional reduction of Differential LL for our fragment is neither confluent nor terminating, as demonstrated by counter examples. This motivated us to this restrict this reduction in two ways.

Reduction is close Only boxes without auxiliary ports may be subject to reduction

Reduction is surface A very limited set of rules may be performed inside boxes

The close constraint allows us to recover confluence, by a technique inspired by the standard proof of confluence for the λ-calculus. On the other hand, being close and surface is not sufficient to ensure strong normalization. This is why we rather prove the property that if we exclude the 0 → rule, then any weakly normalizing net is strongly normalizing. This ensure that as long as a net have a normal form in this 0 →-free fragment, then any path of reduction will eventually lead to this normal form.

This completes the study of the abstract rewriting system of nets that has been carried in this chapter. The next chapter focuses on a specific family of nets that plays a key role in the expression of concurrency-related features.

Chapter 3 Routing Areas

Concurrency involves threads and a means of communication between them, be it a shared memory (references), messages (channels) or something else. Such a means of communication, take for example a memory cell in a shared memory, may both have multiple sources (threads writing in this cell) and multiple targets (threads reading this cell). The expected behavior in case of concurrent accesses is dictated by the operational semantic of the source language. In the case of a message channel for example, a read operation could retrieve at random one value amongst all sent messages, or rather the last message sent if channels act as a stack.

To interpret a fragment of π-calculus in nets, [START_REF] Ehrhard | Interpreting a finitary pi-calculus in differential interaction nets[END_REF] introduces communication areas. For an integer n, the n-communication area is a simple net with 2n + 2 free ports, corresponding to inputs and outputs grouped in pairs, that enables a bidirectional communication between the n + 1 processes -or rather, their representation as a net -that are plugged on each input/output pair. In this chapter, we introduce routing areas, which generalize the design of communication areas. The motivation is similar: we aim at crafting special nets to be used as building blocks for implementing communication primitives. While a communication area connects (by default) all processes, a routing area is parametrized by an algebraic object (a multirelation) that allows a finer control over the implemented communication scheme (cf Section 2.6 for a detailed comparison). For example, take three processes P, Q and R communicating through a channel. With a routing area, we can statically enforce various restrictions, such as banning P from sending messages to Q, or banning R from receiving messages from P , depending on the chosen multirelation. One can imagine implementing ownership constraints, in the style of the Rust programming language, where only one process -say P -is able to send messages and every other ones can only listen. Routing areas allow to connect multiple agents with a parametrizable behavior.

Overview Section 3.1 introduces routing areas. In order to do so, various technical tools are introduced first. Section 3.1.1 introduces the notion of multirelation, a quantitative extension of relations between sets, which will be used to give an algebraic description of a routing area. Section 3.1.2 defines (co)contraction trees, which can be seen as generalized n-ary (co)contractions, and derives a corresponding reduction rule. Co(contraction) trees will be the basic ingredients for building routing areas. Section 3.1.3 briefly reviews the correctness criterion which has been mentioned in Chapter 2. It will be used for various proofs of this chapter, as routing areas does satisfy the correctness criterion. Then, everything is in place to construct routing areas, which is done in Section 3.1.4.

Section 3.2 describes constructions that allow to combine simple routing areas into more complex ones. We give two fundamental operations, juxtaposition and trace, and define the composition of routing areas from these two. Section 3.3 observe that the interpretation of routing areas as communication devices extends to a larger class of nets, routing nets, which include routing areas. The necessity of recasting the notion of connection between endpoints in this setting leads us to give a formal treatment of path in Section 3.3.1. This tool allows to prove in Section 3.3.2 that the normal form of a routing net is a routing area. This provides a semantics that associates the multirelation describing its normal form to a routing nets. We study the properties of this semantics in Section 3.3.3, and show that it is closely related to paths.

Routing Areas

Contraction, weakening, cocontraction and coweakening act as resource dispatchers (a resource designates a closed exponential box in the following). Structural rules are a natural choice for the basic components of routing areas.

•

A wire acts as the identity. It passively forwards a resource that is connected on the input (the left port) to the output (the right port).

• ? A contraction is a broadcaster with one input and two outputs. A resource connected on the left will be copied to both outputs on the right. A weakening is a degenerate case of a broadcaster with zero outputs as broadcasting something to no one is the same as erasing it.

• ! Dually, a cocontraction is a packer with two inputs and one output. A packer aggregates its two inputs non deterministically. When a dereliction is connected to the output to consume two packed resources, a non-deterministic sum of the two possible choices for the resource to be provided is produced. Similarly, coweakening is seen as a degenerate packer with no inputs.

A routing area can be seen as a wiring between inputs and outputs. Inputs are connected to contractions which broadcast the resources they receive to cocontractions. Cocontractions may gather resources from multiple such sources. The conclusions of these cocontractions form the outputs.

Multirelations

In order to describe a routing area, we rely on a natural generalization of a relation between sets, a multirelation. Its role is to define the wiring diagram, which specifies which inputs and outputs will be connected in the routing area. A multirelation between two sets is a relation with multiplicity. Instead of just indicating if two elements x and y are related or not, a multirelation associates an integer n ∈ N to the couple (x, y). If the value at (x, y) is 0, then x and y are not in relation. Otherwise, the value n ≥ 1 quantifies how much, or rather how many times, x and y are in relation.

. Relations and multirelations

A relation between A and B can be seen as a multirelation whose value at a pair (x, y) is either 0, meaning "not in relation", or 1, meaning "in relation". Formally, the map that takes a relation R and returns its characteristic function ρ : R → 1 R is an injection from relations between A and B to multirelations between A and B. Conversely, we can forget the multiplicity of a multirelation S and simply take 0 to mean not in relation and n ≥ 1 to mean in relation. Doing so, we recover a relation from a S through the map ν :

S → {(x, y) ∈ A × B | S(x, y) ≥ 1}. Note that ν is the left inverse of ρ : ν • ρ = id .
From now on, we only consider multirelations between finite sets. Definition 3.1.3. Arity Let R be a multirelation between (finite) sets E and F . We define the arity of e ∈ E as the total number of times it is in relation with an element of F , with multiplicity: ar(e) = f ∈F R(e, f ). Similarly, the arity of f ∈ F is defined by ar(f ) = e∈E R(e, f ). The set of elements of

F (resp. E) connected to e ∈ E (resp. f ∈ F ) is defined by co(e) = {f ∈ F | R(i, o) > 0} (resp. co(f ) = {e ∈ E | R(e, f ) > 0}). Remark 3.1.4. For x ∈ E ∪ F , ar(x) ≥ |co(x)|. ar(x) = |co(x)| for all x ∈ E ∪ F if and only if R is a relation.
A composition operation can be defined on multrelations, which computes all the ways to go from an element to another with multiplicities.

(S • R)(x, z) = y∈B R(x, y)S(y, z)
This composition is associative, coincides with the usual one for relations, and has the identity relation (seen as a multirelation) for neutral. One can view a multirelation as a |B| × |A| matrix with integers coefficients. Lines (resp. columns) are indexed by elements of B (resp. A). For (a, b) ∈ A × B, the coordinate R b,a is equals to R(a, b). Under this interpretation, the composition previously defined on multirelations corresponds to the matrix multiplication. Proposition 3.1.6. The FMRel category Finite sets and multirelations between them form a category FMRel with the composition defined above, which contains the category FRel of finite sets and relations as a subcategory. FMRel has finite coproducts.

Proof. Proposition 3.1.6 This can be showed directly from the defintions, but under the interpretation of multirelations between finite set as finite matrices with positive integer coefficients, one realizes that FMRel is actually the category of integer matrices, which has direct sums as coproducts.

Multirelations are used to describe routing areas. In order to build a routing area from this description, we need to build dispatchers (resp. packers) with an arbitrary number of outputs (resp. inputs). The notion of contraction (resp. cocontraction) tree -consisting in several contraction (resp. cocontraction) stacked together -is the natural construction for this role. We define them and give the laws governing their reduction.

(Co)contraction trees

Remark 3.1.7. In this whole chapter, we consider two additional atomic rules for the reduction accounting for the neutrality of (co)weakening for (co)contraction:

! ! n → ? ? n →
As discussed in the coming Section 3.1.3, all the nets considered in this chapter satisfy a correctness criterion. In this context, confluence and strong normalization of nets is ensured and remains true when one also include the n → rules [START_REF] Tranquilli | Nets between determinism and nondeterminism[END_REF][START_REF] Tranquilli | Intuitionistic differential nets and lambda-calculus[END_REF]. Without these rules, one would have to consider a notion of (co)contraction trees, and consequently of routing areas, with infinitely many distinct representatives. While these rules are not strictly necessary to our developments, it surely comes in handy by forcing the uniqueness of several objects introduced in the following.

A n-ary (co)contraction tree is a stack of (co)contraction defined by induction, represented in the following way:

We will sometimes omit the arity, but always represent the dots between auxiliary ports to differentiate from (co)contraction and (co)weakening cells. Definition 3.1.8. (Co)contraction tree Let n ∈ N, we define an n-ary (co)contraction tree as a simple net with n + 1 free ports, split between a principal port and auxiliary ports. All wires are labelled by the same formula !A (or ?A ⊥ depending on the orientation). (Co)contraction trees are defined by induction:

• n = 0: a 0-ary tree is a (co)weakening, the principal port being the principal port of this (co)weakening.

• n = 1: a unary tree is a wire. If it has ports p 1 and p 2 , the principal port is set to be the p j such that the label of (p j , p 2-j ) is ?A ⊥ (resp. !A in the case of cocontraction tree).

• n > 1: a n-ary tree for n > 1 is built from a (n -1)-ary tree by connecting one of its auxiliary port to a (co)contraction. Commutativity and associativity of (co)contractions ensure that the result does not depend on the choice of the auxiliary port.

On (co)contraction trees, we define merging and reduction, as follows:

Proposition 3.1.9. Tree merging Let n ≥ 0 and m ≥ 1. Connecting the main port of a (co)contraction tree of arity n to an auxiliary port of a (co)contraction tree of arity m yields a (co)contraction tree of arity p = n + m -1:

Proof. By easy induction on n.

When a contraction tree and cocontraction tree are connected through their principal port, one can derive the following generalized reduction rule: The last tool we introduce is the correctness criterion.

Correctness criterion

The correctness criterion is a property of simple nets which, when verified, ensures strong normalization. In Chapter 2, we studied nets that may not satisfy this correctness criterion. Instead, the communication devices that we define in this chapter are correct nets. Let us review the correctness criterion, which we have adapted for our case of nets only composed of contraction, cocontraction, weakening and coweakening. Definition 3.1.11. G(R) and switching graphs Let R be a simple net, we define the graph G(R) = (V, E) by:

• The set of vertices V is the disjoint union of the set of cells of and the set of free ports of R.

• For each wire w of S, we add an edge {v 1 , v 2 } in E where v 1 (resp. v 2 ) is either the cell containing src(w) (resp. tgt(w)), or simply src(w) itself (resp. tgt(w)) if it is a free port.

A switching graph S = (V, E s ) is a graph obtained from G(R) by removing, for each contraction, exactly one of the two wires (formally one of the two corresponding edges in E) connected to its two auxiliary ports.

Definition 3.1.12. Correctness criterion A simple net R verifies the correctness criterion if all its switching graphs are acyclic. In this case, R is said to be correct. We are finally ready to introduce routing areas.

Routing areas

A routing area is a simple net which is described by a multirelation between its inputs and outputs, which are a partition of its free port. The value of the multirelation at the pair (i, o) indicates how many times the input i is connected to the output o.

Definition 3.1.14. Routing area Let L i and L o be two finite sets called the input labels and the output labels.

Let R be a multirelation between L i and L o . The routing area described by the triplet

(L i , L o , R) is a pair (R, σ)
where R is a simple net R and σ -the labelling map -is a bijection from the set of free ports of R to L i + L o , partitioning the free ports between inputs -whose labels are in L i -and outputs, whose label are in L o . R is constructed in the following way:

• Each input i is connected by a wire to the principal port of a contraction tree of arity ar(σ(i)).

• Each output o is connected by a wire to the principal port of a cocontraction tree of arity ar(σ(o)).

• Let (i, o) ∈ L i × L o and n = R(i, o) (remember that n is an integer). Then there are exactly n distinct wires (p i , p i ) connecting auxiliary ports of the contraction tree of i to auxiliary ports of the cocontraction tree of o.

Remark 3.1.15. Notations For a routing area (R, σ) described by (L i , L o , R), σ is a bijection between the free ports of R and L i + L o . We will freely assume that the free ports of R are actually L i + L o , and do not bother with σ anymore. Up to isomorphism and equivalence, the net R is uniquely defined by its description. When unambiguous, we will abuse the notation and write R = (L i , L o , R) to mean that there exists σ such that (R, σ) is the routing area described by (L i , L o , R).

Remark 3.1.16. Communication Areas

The communication areas defined in [START_REF] Ehrhard | Interpreting a finitary pi-calculus in differential interaction nets[END_REF] are a special case of routing areas: for n ≤ 1, the n-communication area is the routing area ({1, . . . , n}, {1, . . . , n}, R) where x R y ⇐⇒ x = y.

Remark 3.1.17. Canonicity of the description of a routing area The multirelation defining an area is not unique from a set-theoretic point of view: indeed, for

R = (L i , L o , R), then the class of multirelations describing R is {τ -1 • R • σ : E → F | σ : E → L i , τ : F → L o , σ and τ bijective }.
Even though this is a proper class, all these multirelations are isomorphic (for example, in the arrow category of FMRel). Finite deterministic automata also suffer this kind of subtlety for example, which is not relevant in practice.

We can make the following basic observations about routing areas:

Proposition 3.1.18. Let R be a routing area, then:

• R is a normal form.

• R is correct.

Proof. Proposition 3.1.18

The fact that a routing area is a normal form is immediate from its shape : contraction and cocontraction trees are only connected through auxiliary ports.

For correctness, observe that in switching graphs, only one branch of each contraction tree may survive. Switching graphs have the following shape:

We represented trees as just one multi-ary node, and long branches corresponding to contraction trees as just one node. We see that this is a forest, a disjoint union of trees, which is acyclic.

We represent routing areas as rectangular boxes, with the inputs appearing on the left and the outputs on the right.

R(i, o) = 2 R(i, o ) = 1 R(i , o) = 0 R(i , o ) = 1
Then the routing area described by (L i , L o , R) is:

Operations on Routing Areas

In this section, we introduce elementary operations on routing areas which allow to combine them:

1. Juxtaposition

Trace

These two operations allows to implement composition, in a way which is similar to the composition of Game Semantic or Geometry of Interaction whose motto is "composition = parallel composition plus hiding".

Juxtaposition The first operation, juxtaposition, amounts to put side by side two routing areas. The result is immediately seen as a routing area itself, described by the coproduct of the two multirelations: Trace The second operation, trace, consists in connecting an input to an output under the condition We ask that the given input and output are not connected, to avoid the creation of a cycle. Doing so, we remove this output and input from the external interface, and create new connections between remaining inputs and outputs. The resulting net reduces to a routing area whose multirelation is defined by Equation (3.1). Definition 3.2.2. Pretrace Let R be a routing area and (i, o) The consistence of Definition 3.2.4 is ensured by Proposition 3.2.3. As routing areas are normal forms, when one forms PreTr (i,o) (R), there can only be one potential redex, created by the connection of i to o. This redex is composed of a contraction tree facing a cocontraction tree, that we know how to reduce thanks to Proposition 3.1.10. We then check that the resulting net is a routing area whose multirelation verifies the equation (Equation (3.1)).

Definition 3.2.1. Juxtaposition Let R = (L i , L o , R) and S = (L i , L o , S), we define the juxtaposition R + S by (L i + L i , L o + L o , R + S).
∈ L i × L o such that R(i, o) = 0. The pretrace of R at (i, o), PreTr (i,o) (R),
∈ L i × L o such that R(i, o) = 0. Then: • PreTr (i,o) (R) satisfies the correctness criterion • PreTr (i,o) (R) → * S

Proof. Proposition 3.2.3

The fact that the pretrace is a correct net is easily deduced from the shape of switching graphs as forests illustrated in the proof of Proposition 3.1.18. It suffices to note that the condition R(i, o) = 0 entails that in any switching graph, the input i and the output o are in distinct trees. The connection of i and o then amounts to connect a leaf of one of those trees to the root of another one, which preserves the forest structure of the switching graph. Thus the switching graphs of the pretrace at (i, o) are also ayclic.

By forming the pretrace at (i, o), we connect the contraction tree of i to the cocontraction tree of o. We apply Proposition 3.1.10 on the introduced redex to get:

where the ports i 1 , . . . , i p are connected to auxiliary ports of trees of the inputs in co(o) and o 1 , . . . , o q to the trees of the outputs in co(i). By Proposition 3.1.9, we can merge all these trees with the one they are connected to such that the reduced net has the shape of a routing area S = (L i , L o , S).

To explicit the multirelation S, we have to determine the number of connections between any input x ∈ L i and output y ∈ L o . The free ports of S are inherited from R, excepted that i and o are now gone: thus

L i = L i \ {i} and L o = L o \ {o}.
The direct connections between x and y in R when x = i and y = o are inherited by S, as they are left unchanged by the reduction. But any pair of connections in R between x and o arriving at some i k , and between i and y arriving at some o l , yields exactly one new connection between x and y in S after the tree reduction. By definition, there are R(x, o) connections between x and o and R(i, y) connection between i and y : there are R(x, o)R(i, y) such couples. The total number of connections between x and y is then S(x, y) = R(x, y) + R(x, o)R(i, y).

Composition Composition consists in connecting the output of an area to an input of another area and reducing the result to a routing area. Let (L i , L o , R) and (L i , L o , S) be two routing areas, o ∈ L o , i ∈ L i , the composition of R and S at (i, o) is defined as the routing area obtained by first taking the juxtaposition of R and S, and then the trace at (i, o). Juxtaposition, trace and composition are fundamental features of routing areas. This is what makes them modular, allowing to build complex routing areas by connecting simple blocks.

Transit We conclude this section with a property that reflects the high level operational behavior of a routing area. It supports our interpretation of routing areas as resource dispatchers. Given a closed exponential box, we connect it to the auxiliary port of a cocontraction to obtain a module which can then be connected to an input i. Through reduction, the box will traverse the area and be duplicated R(i, o) times to each output o. The role of the additional cocontraction is to preserve the area and allow future connections to the same input. We would get a similar transit property by connecting directly the exponential box to i, but this process is destructive as it would erase the input wire of i and prevents any future usage.

Proposition 3.2.7. Transit Let σ be a closed exponential box, R = (L i , L o , R) a routing area, i ∈ L i . Let {o 1 , . . . , o p } = co(i) and for 1 ≤ k ≤ p, c k = R(i, o k ). Then : Proof. Proposition 3.2.7
If we consider the added cocontraction as a 2-ary tree, we can apply Proposition 3.1.10. We aggregate them with the cocontraction trees of outputs using Proposition 3.1.9. Then we duplicate the exponential boxes now facing cocontraction tree several times using The last section of this chapter is dedicated to generalize the ideas and the approach developed for routing areas to a larger class of nets, routing nets.

Routing Nets

Routing areas are specific normal forms of nets composed of structural cells, which are contraction, cocontraction, weakening and coweakening. We saw (in Section 3.1) that these cells have an interpretation as simple communication devices. We also proposed ways of combining these simple devices into more involved ones, and that the communication interpretation -practically, the description as a multirelation between inputs and outputs -apply to these combinations. This leads us to wonder if this interpretation can be extended to more general assemblies of structural cells: can any net constituted of structural cells, not necessarily in normal form and not necessarily a combination of routing areas, be seen as a communication device and described as such by a multirelation in the same way as a routing area ? The answer given in this section is yes, as long as nets are correct. More precisely, we show that correct nets composed of structural cells, routing nets, reduce to a routing area. We can thus associate to any such net the multirelation describing its normal forms.

Section 3.3.1 does a formal treatment of paths in simple net, an ubiquitous concept in the section. They allow us to speak and quantify connections between free ports in the more general setting of routing nets, instead of just routing areas. We show that the correctness of routing nets exclude the existence of a cyclic path, which is a cornerstone of the proof that the normal form of a routing net is a routing area (Theorem 3.3.7). This theorem is proved in Section 3.3.2. Section 3.3.3 ends the section by exploring the consequence of the fact that routing nets reduce to routing area, which is that we can define a semantics that associate the multirelation describing its normal form to a routing net. Its properties are studied, and we give an alternative formulation in terms of paths that is independent from routing areas. Definition 3.3.1. Routing nets A routing net R is a net whose cells are weakenings, coweakenings, contractions or cocontractions that satisfies the correctness criterion. Moreover, we ask that all wires are labelled with the same formula !A, fixing de facto their orientation.

Note that routing area are a special case of routing nets.

Paths in Routing Nets

Simple nets can be seen as graphs where vertices are cells and edges are wires: this is the graph G(R) introduced in Definition 3.1.11. The notion of path defined below corresponds the standard notion of a path in this graph, with the additional restriction that paths can not "bounce back" on a cell through the principal port or through two auxiliary ports. When a path enters a node through an auxiliary port, it must exit through the principal port, and vice-versa. Similarly, it can not bounce back on a free port.

Let R be a simple net. We recall a few notations. For a cell c of R, we write p i (c) for its i-th auxiliary port if it exists and p(c) for its principal port. For a wire w = (p, p ), src(w) = p designates the source port of w while tgt(w) = p is its target port. The undirected graph G(R) = (V, E) is constructed as follows:

• The set of vertices V is the disjoint union of the set of cells of and the set of free ports of R.

• For each wire w of S, we add an edge (v where v i is a vertice of G(R) and e i is an edge between v i and v i+1 . We can associate to π a corresponding sequence (w 1 , . . . , w n ) of wires of R oriented such that src(w i ) = v i and tgt(w i ) = v i+1 . A non bouncing path, or just path in the following, is such a sequence π such that for i < n, tgt(w i ) and src(w i+1 ) must not be either:

• Both auxiliary ports of the same cell.

• Both principal ports of the same cell.

• Both free ports.

We define src(π) = v 1 and tgt(π) = v n+1 . For two free ports p 1 and p 2 ,

Paths p 1 →p 2 (R) = {π | π path , src(π) = p 1 , tgt(π) = p 2 }
is the set of paths starting at p 1 and ending at p 2 .

There is a relation between correctness and the paths we have defined. We show that a routing net, because it is correct, does not contain cyclic paths. Proposition 3.3.3. Acyclicity of correct nets A routing net is acyclic, that is there is no path π such that src(p) = tgt(p).

The proof requires the following lemma: Lemma 3.3.4. Path invariant Let R be a simple net, G(R) = (V, E) be the associated graph, σ = (v 1 , e, v 2 ) a path, w = (p 1 , p 2 ) the corresponding wire in R and F its label. We define the polarity pol(σ) by:

• If F = ?A, pol(σ) = -. • If F = !A, pol(σ) = +.
Then, for a path π = (v 1 , e 1 , . . . , e n , v n+1 ), the polarity is constant along π, meaning that for 1 ≤ i, j ≤ n, pol((v i , e i , v i+1 )) = pol((v j , e j , v j+1 )).

Proof. Lemma 3.3.4

The non bouncing condition enforces that two consecutive subpaths (v i , e i , v i+1 ) and (v i+1 , e i+1 , v i+2 ) must have the same polarity. We conclude by induction on the length of the path.

Proof. Proposition 3.3.3 We prove that the existence of a cycle implies the existence of a cycle in a switching graph. More precisely, we show that a minimal cycle never visits the two auxiliary ports of a contraction and that it is thus contained in some switching graph.

Assume the existence of a cycle and select one of minimal length, σ. We will rather work on the associated sequence of oriented wires (w 1 , . . . , w n ). Assume that the two wires connected to the auxiliary ports of some contraction c, f and f , are both visited by σ. There must be two indices i 0 and i 1 such that w i 0 = f and w i 1 = f . We can assume i 0 < i 1 , such that σ = (w 1 , . . . , w i 0 -1 , f, w i 0 +1 , . . . , w i 1 -1 , f , w i 1 +1 , . . . , w n ). By the invariance of polarity along a path (Lemma 3.3.4), f and f are visited in the same direction, either both exiting c or both entering c. Moreover, they can not be consecutive in σ by definition of a non bouncing path. Let us extract from the subpath (f, w i 0 +1 , . . . , w i 1 -1 , f ) a cycle strictly smaller than σ. If both f and f are exiting c, then the path must enter c by the principal port, thus w i 1 -1 must correspond to the wire that contains the principal port of c. But then (f, w i 0 +1 , . . . , w i 1 -1 ) is a cycle strictly smaller than σ. Similarly, if both are entering c, then (w i 0 +1 , . . . , f ) is a cycle strictly smaller than σ. Hence, a minimal cycle σ does not visit both auxiliary ports of a contraction cell, and is contained in at least one switching graph.

We now give an important property relating reduction to paths. It states that paths that are long enough -here paths that start and end at a free portare preserved by the reduction. Proof. Proposition 3.3.5 For a path π, the principal port p of a weakening or a coweakening constitute a dead end: if π visits p, p must be either the source or the target of π. As a path in Paths p 1 →p 2 (R) starts and ends at a free port, it can not visit a (co)weakening. The reductions implying (co)weakenings thus leave such paths unchanged. The only reduction affecting paths in Paths p 1 →p 2 (R) is the ba → rule:

Subsequence Image by τ i 1 , c, o 1 i 1 , c 1 , o 1 i 1 , c, o 2 i 1 , c 2 , o 2 i 2 , c, o 1 i 2 , c 3 , o 1 i 2 , c, o 2 i 2 , c 4 , o 2
We omitted the four dual possibilities which can be deduced from this table by reversing both the subsequence and its image. It is easily seen that τ is bijective.

We can now reformulate the link between a routing area R and its defining relation R in terms of paths: R(i, o) is the number of distinct paths linking i to o. Proposition 3.3.6. Paths in routing areas Let R = (L i , L o , R) be a routing area and (i, o)

∈ L i × L o . Then R(i, o) = |Paths i→o (R)|.
Paths allow to generalize the notion of an input and an output being connected in a routing area. We can replace it by the existence of a path between any two free ports in a routing net. This allows us to prove in the next subsection that routing nets are actually, up to normalization, routing areas.

Normal forms

In this section, we show that routing areas are the normal forms of routing nets. That means that an arbitrary routing net always reduces to a routing area. Observe that the basic components of routing nets, (co)contractions, wires and (co)weakenings are all routing areas. From there, we show that we can combine them into an arbitrary routing net using pretrace and juxtaposition. Thanks to Proposition 3.2.3, this implies that the resulting net reduces to a routing area that can be expressed as trace and juxtaposition of basic cells. One of the key ingredient of the proof is to justify that the trace operations are legal, as Tr (i→o) (.) is defined only when i and o are not connected: this is where we make use of paths, which enable to speak about connection formally. • (induction step) Let take any cell c of R. We call R the subnet obtained by removing c from the set of cells of R.

By induction, R can be reduced to a routing area R . Then, depending on the nature of c:

(co)weakening If c is a weakening or a coweakening, it is a routing area and can be composed with R , and reduced to a new routing area R according to Definition 3.2.5. Thus the whole net reduces to R.

(co)contraction If c is a contraction or a cocontraction, it is also a routing area and we juxtapose it to R . If we then perform thee traces operations to reconnect the ports of c one by one, we obtain a routing area which is a reduct of the original net R. What we need to check is that trace operations are legal, as they are only defined when the input and the output at which we perform the operation at are not connected -or, put differently, that there is no path between them -in the corresponding intermediate routing areas. The first operation is always legal, as it is actually a composition of disjoint areas. For the remaining two, if a path existed between two ports in an intermediate routing area, this path already existed in R by Proposition 3.3.5. But this would result in a cycle in R, which is excluded by Proposition 3.3.3. Thus the trace operations are legal.

We can thus associate to a routing net the routing area that is its normal form. This area being described by a multirelation, we derive from our study of routing areas a semantics for routing nets.

The Routing Semantics

For a routing net S, we define the application . : S → R that maps S to the multirelation R describing its normal form. By unicity of normal forms, the application is invariant by reduction and is thus a semantics for routing nets, with the following properties:

Sound The multirelation only depends on the normal form. As the reduction is confluent, the normal form of a routing net is unique, and . is invariant by reduction.

Adequate Two routing nets with the same denotation have the same normal form, as a multirelation defines a routing area uniquely up to isomorphism.

Fully complete Any multirelation on finite sets is realised by the associated routing area.

Compositionnal We can compute the semantics of a net in a compositional way from the semantics of its smaller parts, and combine them through juxtaposition, trace and composition.

Proposition 3.3.6 formalizes the idea that the multirelation describing a routing area is determined by paths between free ports: the value on a pair (i, o) is the number of paths between them. This interpretation extends to routing nets: for a routing net R, its normal form have the same free ports as S. They can be seen as inputs and outputs, and R can be computed by counting the paths between the free ports directly in R: • If S is a normal forms, then it is a routing area, and this was already noted for routing areas in Proposition 3.3.6.

• Otherwise, by path preservation (Proposition 3.3.5), N (i, o) is invariant by reduction. We conclude by induction on the length of a reduction of S to its normal form.

Taking a step back, the routing semantics relies on the fundamental observation that specific sets of paths are preserved by reduction and totally determines the normal form of a net. The equivalence we set on simple nets, namely associativity and commutativity of (co)contraction, makes two paths from a free port to another one indistinguishable in the normal forms. This is why we can ignore the structure of these paths and simply count them.

Summary

This chapter introduced and studied routing areas, which are simple nets designed to implement communication primitives. Routing areas are inspired by communication areas introduced in [START_REF] Ehrhard | Interpreting a finitary pi-calculus in differential interaction nets[END_REF]. We show that routing areas are modular, as they can be composed in different ways such that the result still reduce to a routing area. The chapter ends by showing that routing areas are actually the language of normal forms of more general nets, routing nets. Any correct net, composed of contraction, cocontraction, weakening and coweakening is in fact a routing area up to normalization. From this result, we derive a semantics for routing nets, the routing semantics. It associates to any routing net a multirelation describing it. This semantics can be defined solely in terms of paths: computing the denotation of a routing nets amount to count specific paths in this net.

Discussion

Communication areas vs routing areas For an integer n, the n-communication area is a simple net with 2n + 2 free ports, corresponding to inputs and outputs grouped in pairs. The n-communication area enables a bidirectional and indiscriminate communication between the n processes which plugged in. For a given n, the associated communication area is unique, and allow any process to communicate with any other one. If we connect several process by a communication area, then each one of them is able to send messages to or receive messages from the others indiscriminately. On the other hand, there exists many routing areas that connect n processes: thanks to the parametrization by a multirelation, we can configure the read/write permissions on process by process basis. For example, we can require that sending messages is forbidden for all processes but one, or rather give the send/receive capabilities on a process-by-process basis. This gives the ability to statically encode various communication scheme of concurrents languages.

This capacity is put to use in Chapter 5, where we propose a translation of a concurrent calculus inside nets. We give an adequacy theorem that formalizes the fact that the translation of a term can not produce "more result" that the original term. If a term either reduces to 1 or 2, then adequacy guarantee that its translation will not reduces to (the translation of) 3 for example. Adequacy relies on the specialization of routing areas to match the calculus semantics: if we used communication areas instead, due to them being more permissive, the translation in nets would be able to compute more than the initial term.

Modularity An important feature of routing areas is their modularity. They can be assembled and connected, as the electric component of a circuit, in various ways such that the result is still a routing area, up to normalization. Modularity is illustrated by the operations defined on them, juxtaposition, trace and composition. This allows to build compositional translations without requiring the knowledge of a whole source program at once to perform the transformation. In other words, this gives routing areas the capability of supporting separate compilation.

Paths in routing nets

The chapter ends by showing that routing areas are actually the language of normal forms of more general nets, routing nets. Any correct net, composed of contraction, cocontraction, weakening and coweakening is a routing area up to normalization. The proof of this fact exposes that routing nets are somehow the "free structure" generated by structural cells as constants and juxtaposition and pretrace as operations. This instills the idea that an arbitrary piece of proof composed only of structural rules is all about wiring. This is reflected by the fact that the routing semantics can be defined directly in terms of paths. Paths are known to be a central notion in nets -and λ-calculus -both dynamically and semantically. They unifies Levy's optimal reduction, Lamping's graph-reduction algorithm and Girard's Geometry of Interaction [START_REF] Asperti | Paths in the lambdacalculus. three years of communications without understanding[END_REF]. While multirelations and routing areas are designed with practical goal in minds, we have seen paths naturally emerging as one tries to extend these ideas to routing nets.

We are now armed to encode various communication primitives inside proof nets. This is illustrated in Chapter 5 by the translation of the λ cES calculus, described in Chapter 4.

Chapter 4

The concurrent λ-calculus with explicit substitutions λ cES

The λ-calculus is a versatile framework in the study and design of higher-order functional programming languages. One of the reasons of its widespread usage is the fact that it can easily be extended to model various computational side-effects. Another reason comes from its theoretical ground and the fine granularity it allows in the design of abstract machines to express various reduction strategies. These abstract-machines can then serve as foundation for the design of efficient interpreters and compilers.

A specially useful tool in the design of such abstract machines is the notion of explicit substitution, a refinement over β-reduction. The β-reduction of the λ-calculus is a meta-rule where substitution is defined inductively and performed all at once on the term. But its implementation is a whole different story: to avoid size explosion in presence of duplication, mechanisms such as sharing are usually deployed. Abstract machines implement various specific strategies that may either be representable in pure λ-calculus (call-by-value or call-byname) or for which the syntax needs to be augmented with new objects (e.g. call-by-need or linear head reduction). The mismatch between β-reduction and actual implementations can make the proof of soundness for an evaluator or a compiler a highly nontrivial task. The heart of the theory of explicit substitutions, introduced in [START_REF] Abadi | Explicit substitutions[END_REF], is to give substitutions a first class status as objects of the syntax to better understand the dynamics and implementation of β-reduction. It consists in decomposing a substitution into explicit atomic steps. The main ingredient is to modify the β rule so that (λx.M )N reduces to M [N/x], where [N/x] is now part of the syntax. Additional reduction rules are then provided to propagate the substitution [N/x] to atoms.

Studied for the last thirty years [START_REF] Abadi | Explicit substitutions[END_REF][START_REF] Accattoli | Proof nets and the call-by-value λ-calculus[END_REF][START_REF] Accattoli | A nonstandard standardization theorem[END_REF][START_REF] Accattoli | leftmost-outermost) beta reduction is invariant, indeed[END_REF][START_REF] Accattoli | The structural λ-calculus[END_REF][START_REF] Gabbay | A new approach to abstract syntax involving binders[END_REF][START_REF] Kesner | A theory of explicit substitutions with safe and full composition[END_REF][START_REF] Lescanne | Explicit substitutions with de bruijn's levels[END_REF][START_REF] Høgsbro | Explicit cyclic substitutions[END_REF][START_REF] Sinot | Efficient reductions with director strings[END_REF], explicit substitution turns out to be a crucial device when transitioning from a formal higher-order calculus to a concrete implementation. It has been considered in the context of sharing of mutual recursive definitions [START_REF] Høgsbro | Explicit cyclic substitutions[END_REF], higher-order unification [START_REF] Lescanne | Explicit substitutions with de bruijn's levels[END_REF], algebraic data-types [START_REF] Gabbay | A new approach to abstract syntax involving binders[END_REF], efficient abstract machines [START_REF] Accattoli | Proof nets and the call-by-value λ-calculus[END_REF][START_REF] Sinot | Efficient reductions with director strings[END_REF], cost-model analysis [START_REF] Accattoli | leftmost-outermost) beta reduction is invariant, indeed[END_REF], etc. The use of explicit substitutions however comes at a price [START_REF] Kesner | A theory of explicit substitutions with safe and full composition[END_REF]. Calculi with such a feature are sensitive to the definition of reduction rules. If one is too liberal in how substitutions can be composed then a strongly normalizing λ-term may diverge in a calculus with explicit substitutions [START_REF] Mellies | Typed λ-calculi with explicit substitutions may not terminate[END_REF]. If one is too restrictive, confluence on metaterms is lost [START_REF] Curien | Confluence properties of weak and strong calculi of explicit substitutions[END_REF]. The challenge is to carefully design the language to implement desirable features without losing fundamental properties. Several solutions have been proposed to fix these defects [START_REF] Accattoli | The structural λ-calculus[END_REF][START_REF] Kesner | A theory of explicit substitutions with safe and full composition[END_REF] for explicit substitutions of term variables.

This chapter introduces an extension of explicit substitutions to a novel case: a lambda-calculus augmented with concurrency and references. Such a calculus forms a natural model for shared memory and message passing. We aim at proving that a translation of a shared memory model to a message passing one is sound.

Strong Normalization in a Concurrent Calculus with References A concurrent lambda-calculus with references -referred as λ C below -has been introduced by Amadio in [START_REF] Amadio | On stratified regions[END_REF]. It is a call-by-value λ-calculus extended with:

• a notion of threads and an operator for parallel composition of threads,

• two terms set(r, V ) and get(r), to respectively assign a value to and read from a reference,

• special threads r ⇐ V , called stores, accounting for assignments.

When set(r, V ) is reduced, it turns to the unit value * and produces a store r ⇐ V making the value available to all the other threads. A corresponding construct get(r) is reduced by choosing non deterministically a value among all the available stores. For example, assuming some support for basic arithmetic consider the program (λx.x + 1) get(r) set(r, 0) set(r, 1). It consists of 3 threads: two concurrent assignments set(r, 0) and set(r, 1), and an application (λx.x + 1) get(r). This programs admits two normal forms depending on which assignment "wins": the term 1 * * r ⇐ 0 r ⇐ 1 and the term 2 * * r ⇐ 0 r ⇐ 1. Despite the operator being a static constructor, it can be embedded in abstractions and thus dynamically liberated or duplicated. For example, the term (λf.f * f * ) act like a fork operation: if applied to M , it generates two copies of its argument in two parallel threads M * M * . Coupled with the Landin's fixpoint introduced below one can even write a fork bomb, that is a non terminating term which spans an unbounded number of threads.

In this language, the stores are global and cumulative: their scope is the whole program, and each assignment adds a new binding that does not erase the previous one. Reading from a store is a non deterministic process that chooses a value among the available ones. References are able to handle an unlimited number of values and are understood as a typed abstraction of possibly several concrete memory cells. This feature allows λ C to simulate various other calculi with references such as variants with dynamic references or communication [START_REF] Madet | Complexité Implicite de Lambda-Calculs Concurrents[END_REF].

While a simple type system for usual λ-calculus ensures termination, the situation is quite different in a language with higher-order references. The so called Landin's trick [START_REF] Peter | The mechanical evaluation of expressions[END_REF] allows to encode a fixpoint in the simply typed version of a calculus with references. The problem lies in the fact that one can store in a reference r values that can themselves read from the reference r, leading to a circularity. For example, the term get(r) * r ⇐ (λx.get(r) * ) loops while involving only simple types Unit and Unit → Unit.

In order to address this issue, type and effects systems have been introduced to track the potential effects produced by a term during its evaluation. Together with stratification on references [START_REF] Boudol | Typing termination in a higher-order concurrent imperative language[END_REF], one can recast termination in such an imperative context. Intuitively, stratification imposes an order between references: a reference can only store terms that access smaller ones, ruling out Landin's fixpoint. Formally, this allows to apply the usual reducibility argument to a calculus with references: stratification ensures that the inductive definition of reducibility sets on types with effects is well-founded.

While scheduling is explicitly handled through language constructs in [START_REF] Boudol | Typing termination in a higher-order concurrent imperative language[END_REF], λ C 's liberal reduction allows to chose a different thread to operate on at any time. This cause additional difficulty, as from a single thread's point of view, arbitrary new assignments may become available between two reduction steps. For λ C , the proof of termination in [START_REF] Amadio | On stratified regions[END_REF] resorts to what amounts to infinite terms with the notion of saturated stores.

In this chapter, we introduce a concurrent λ-calculus with explicit substitution, based on the λ C calculus. We provide a stratified type and effect system for this calculus, and show that typing ensures strong normalization.

Overview In Section 4.1, we introduce the concurrent λ-calculus with explicit substitutions λ cES , with both substitutions for variable and references. The syntax of terms is spelled out in Section 4.1.1, while the reduction is given in Section 4.1.2. In Section 4.1.4, we define a partial preorder on terms, which will be used to compare the behaviors and the normalization of terms in the following sections.

In Section 4.2, we introduce a stratified type and effect system for λ cES , adapted from the one of λ C . We show basic properties of the typed fragment, such as subject reduction and progress, in Section 4.2.2.

In Section 4.3, we prove an important result of this chapter, which is that well typed terms are strongly normalizing. To do so, we adapt a reducibility proof to our setting by incorporating an interactive properties. In Section 4.3.1, we lay out some necessary technical definitions, such as sets of strongly computable terms and our interactive condition of being a well-behaved term. We give a high level explanation of the proof in Section 4.3.2, and detail two representative cases. In Section 4.3.3, we give a more detailed proof of the strong normalization theorem and other intermediate results.

At last, Section 4.4 focuses on the relation between λ cES and λ C . While λ cES should be thought of as a version of λ C with explicit substitutions, the latter is not a proper sublanguage of the former. We can however define a translation, or rather an embedding, of λ C in λ cES . We prove a simulation for this embedding in Section 4.4.2. We explain why a simulation result in a non-deterministic setting is only half satisfying when one ought to relate the computational behaviors of two languages. In Section 4.4.3, we give an adequacy theorem, which is complementary to the simulation result. It states that the values than can be computed by a term of λ C and the ones that can be computed by its translation in λ cES are essentially the same.

A Concurrent λ-calculus with Explicit Substitutions

In standard presentations of the lambda-calculus and its extensions such as [START_REF] Amadio | On stratified regions[END_REF], substitutions are applied globally. This hides the implementation details of the procedure. Exposing such an implementation is one of the reasons for the introduction of explicit substitutions. In the literature, explicit substitutions have only been used for term variables and not for references.

In this section, we introduce the language λ cES , a call-by-value, concurrent λ-calculus with explicit substitutions for both term variables and references.

Syntax

The language λ cES has two kinds of variables: term variables (simply named variables) represented with x, y, . . ., and references, represented with r, r , . . .. Substitutions are represented by partial functions with finite support. Variable substitutions, denoted with Greek letters σ, τ, . . ., map variables to values.

Reference substitutions, denoted with calligraphic uppercase letters V, U, . . ., map references to finite multisets of values. Multisets reflect the non-determinism, as multiple writes may have been performed on the same reference. They are represented with the symbol E. The language consists of values, terms and sums of terms, representing non-determinism.

-values V ::

= x | * | λx.M -terms M ::= V | M [σ] | (M M )[V] λ | get(r) | M [V] ↓ | M [V] ↑ | M M -sums M ::= 0 | M | M + M
The construct M [σ] stands for the explicit substitutions of variables in M under the substitution σ. There are three constructs for explicit substitutions for references: M [V] ↓ and M [V] ↑ are respectively the downward and upward references substitutions, while (M M )[V] λ is the λ-substitution. The reason for which the language needs three distinct notations is explained in the next section while presenting the reduction rules. Finally, the role of the sum-terms M is to capture and keep all non-deterministic behaviours.

Terms are considered modulo an equivalence relation presented in Table 4.1. The sum is idempotent, associative and commutative, while the parallel composition is associative and commutative. Definition 4.1.1. Free variables The set of free variables FV(M ) of a term M is defined as follow:

• FV(x) = {x} • FV( * ) = ∅ • FV(λx.M ) = FV(M ) \ {x} • FV(M [σ]) = FV(M ) \ dom(σ) ∪ FV(σ) • FV(M N [V] λ ) = FV(M ) ∪ FV(N ) ∪ FV(V) • FV(get(r)) = ∅ • FV(M [V] ↓ ) = FV(M [V] ↑ ) = FV(M ) ∪ FV(V) • FV(M N ) = FV(M ) ∪ FV(N ) • FV(σ) = x∈dom(σ) FV(σ(x)) • FV(V) = r∈dom(V) V ∈V(r) FV(V ) A closed term is a term M such that FV(M ) = ∅. M M = M M (M M ) M = M (M M ) M + M = M + M (M + M ) + M = M + (M + M ) M + M = M + 0 = M Table 4.1: Structural Rules E ::= [.] | (E M )[V] λ | (M E)[V] λ | E[V] ↓ | E[V] ↑ C ::= [.] | (C M ) | (M C) S ::= [.] | S + M | M + S
[r ⇐ V ] to mean [V] with V : r → [V ]. Explicit variables substitutions are written M [{x 1 → V 1 , . . . , x n → V n }].
Finally, by abuse of notation we write (M N ) for (M N )[⊥], where ⊥ is the nowhere defined function.

Reduction

We adopt a weak call-by-value reduction where the reduction order of an application is not specified. It is weak in the sense that no reduction occurs under abstractions.

Although in a general setting non-determinism and call-by-value taken together may break confluence even when collecting all possible outcomes [START_REF] De | Non deterministic extensions of untyped lambda-calculus[END_REF], this phenomenon does not happen here. Indeed, we cannot reduce under abstractions, and the only non-deterministic construct get(r) must be reduced before being duplicated, avoiding problematic interactions between β-reduction and non-deterministic choice.

The language λ cES is equipped with the reduction defined in Table 4.3. The rules presented are closed under the structural rules of Table 4.1. We assume the usual conventions on alpha-equivalence of term, and as customary substitutions are considered modulo this alpha-equivalence. They make use of several notations that we lay out below. Rules devoted to dispatching substitutions are referred as structural rules. The variable (resp. downward, upward ) structural rules consist in (subst) (resp. (subst-r), (subst-r')) rules excluding (subst var ) (resp. (subst-r get ), (subst-r )). An in-depth discussion about these rules follows.

Notation 4.1.4. the contexts E, C and S are defined in Table 4.2. The context E stands for a usual call-by-value applicative context, C picks a thread, while S picks a term in a non-deterministic sum. Note how E does not enforce any reduction order on an application. Notation 4.1.5. Given a variable substitution σ and a value V , we define the value V {σ} as follows: (λx.M ){σ} = λx.(M [σ]), (x){σ} = σ(x) if σ is defined at x or (x){σ} = x if not, and ( * ){σ} = * . Notation 4.1.6. We use the notation X = V, W for the juxtaposition of references substitutions. It is defined by X (r) = V(r) + W(r) if both are defined and where + is the union of multisets, V(r) if only V is defined, and W(r) if only W is defined. We use the same notation for the composition of variable substitutions, defined by (σ, τ

)(x) = σ(x){τ } if both are defined, σ(x) if only σ is defined τ (x) if only τ is defined. Finally, we define V{σ} : r → [V i {σ} | V i ∈ V(r)].
We now give some explanations on the rules of Table 4.3.

(a) β-reduction If one forgets the λ-substitution explained below in (d), this set of rules encapsulates the call-by-value behavior of the language: only values can be substituted in the body of abstractions, and this happens within a thread in a call-by-value applicative context.

(b) Variable Substitutions A variable substitution can be seen as a message emitted by a β-redex and dispatched through the term seen as a tree. The substitution flows from the redex downward the term-tree until it reaches the occurrence of a variable. The occurrence is then replaced, or not, depending on the variable to be substituted. The rules in Table 4.3(a) are an operational formalization of this step-by-step procedure. Consider for example the reduction of the term (λx.x y z) (λx.x). The redex triggers with (β v ) the substitution of all occurrences of x in what was the body of the lambda-abstraction. The substitution goes down the corresponding sub-term and performs the substitution when it reaches an occurrence of x. Remark 4.1.7. On rules (subst subst-r ) and (subst subst-r' ). When composing or swapping substitutions, non-values may appear in unfortunate places: take for example ( *

[V] ↑ )[σ], its reduction should be ( * [σ])[V ] ↑ where V (r) = [V [σ] | V ∈ V(r)] when V(r) is defined. But V [σ]
are not necessarily values and should then be able to be reduced inside substitutions. However, note that V [σ] always reduces in one step to the value V {σ}. To avoid additional complexity, we perform this reduction at the same time, whence the use of V {σ} instead of V [σ] in the actual rules.

(c) Downward Reference Substitutions An assignment can occur anywhere within a term and it must be able to reach a read located in an arbitrary position. In a language such as [START_REF] Amadio | On stratified regions[END_REF], the solution is to keep all assignments in a global store. When a read gets evaluated, the value for the reference is taken from the store. This approach is very global in nature: the store is "visible" by every subterm. The language λ cES features a step-by-step decomposition of reference assignments akin to term variable substitutions: an assignment follows the branches of the term-tree, actively seeking a read. We therefore introduce two sorts of reference substitutions: one that goes downward (indicated by ↓), similar to variable substitutions, and one that goes upward (indicated by ↑). Starting from an assignment, the latter climbs up the tree up to the root. The rules in Table 4.3(c) describe the former while the rules in Table 4.3(d) describe the latter.

Remark 4.1.8. In Table 4.3, the rule (subst-r get ) is the central case of the reduction of reference substitutions. It says that whenever a downward substitution reaches a get(r), then it generates a non deterministic sum of all the available values for the reference r (if V is undefined at r, then this sum is understood as a neutral element 0) plus a term where the substitution was discarded but the get(r) is left unreduced. To see why this "remainder" is necessary, consider the term get(r

)[r ⇐ V 1 ] ↓ [r ⇐ V 2 ] ↓ . If we omit the remainder, the term could reduce to V 1 [r ⇐ V 2 ] ↓ and finally to V 1 . But another reduction is possible: one can first reduce the term to get(r)[r ⇐ V 1 , r ⇐ V 2 ] ↓ and then to V 1 + V 2 .
The get(r) must not be greedy: when it meets a substitution, it has to consider the possibility that other substitutions will be available later. This aspect will be crucial when considering the proof of strong normalization of the language in Section 4.3.

(d) Upward Reference Substitutions Each time an upward reference substitution goes through a multi-ary constructor -as an application or a parallel composition -it propagates downward substitutions in all the children of the constructor except the one it comes from, while continuing its ascension. Eventually, all the leafs are reached by a corresponding downward substitution. To illustrate the idea, consider a term M N where M contains a get(r) somewhere and N an assignment * [r ⇐ V ] ↑ . The reduction of explicit substitutions would go as follows.

M N M . . .

get(r) N . . . * [r ⇐ V ] ↑ M N M . . . get(r) N . . .[r ⇐ V ] ↑ * M N M . . . get(r) N [r ⇐ V ] ↑ . . . * (M N )[r ⇐ V ] ↑ M [r ⇐ V ] ↓ . . . get(r) N . . . * (M N )[r ⇐ V ] ↑ M . . .[r ⇐ V ] ↓ get(r) N . . . * (M N )[r ⇐ V ] ↑ M . . . get(r)[r ⇐ V ] ↓ N . . . * (M N )[r ⇐ V ] ↑ M . . . V N . . . *
One last subtlety in the movement of reference substitutions concerns λabstractions. As made explicit in Table 4.3(a), the language is call-by-value: reduction does not happen under λ-abstractions. In particular, a read within the body of a λ-abstraction should only be accessible by an assignment when the λ-abstraction is opened: we have a natural notion of pure and impure terms. Pure terms are terms that will not produce any effect when reduced, and in particular, all values are expected to be pure terms since they cannot reduce further. This is highlighted by rule (subst-r val ): when encountering a pure term, a reference substitution vanishes. But the case of abstraction is more subtle: computational effects frozen in its body are freed when the abstraction is applied. If one implements naively the reduction rules of reference substitutions, then the following example does not behave as expected: ((λx.get(r)) * )[V] ↓ → ((λx.get(r))[V] ↓ ) ( * [V] ↓ ) → (λx.get(r)) * → get(r). We end up with an orphan get(r) despite the fact that a substitution was available at the beginning. The problem is that the substitution diffuses through the application, then encounters two pure terms and vanishes.

In an application, the left term eventually exposes the body of an abstraction, and this body should be able to use any substitution that was in its scope. The λ-substitution [-] λ is a special stationary reference substitution attached to an application. Its goal is precisely to record all the substitutions that went down through it with Rules (subst-r' lapp ) and (subst-r' rapp ). When the application is finally reduced with a β v -rule, this substitution will turn to a downward one and feed the get(r)'s that were hidden in the abstraction's body. Lemma 4.1.13. Critical pairs We write E 1 #E 2 for two contexts E 1 , E 2 if E 1 = E 2 , and each one is not a prefix of the other, i.e. ∀E,

E 1 = E 2 [E] and E 2 = E 1 [E].
In the following, we write the reduction rules as S[N ] → S[N ] + M , where M is equals to 0 unless when (subst-r get ) occurs, where it may correspond to additional terms.

If M → M 1 and M → M 2 with M 1 = M 2 , then one of the assertion holds :

1. The two rules are of the form

S i [N i ] → S i [N i ] + M i with S 1 #S 2 , M = S i [N i ] = i N i 2.
The two rules are of the form

S[C i [N i ]] → S i [C i [N i ]]+M i with C 1 #C 2 , C i [N i ] = i N i 3. The two rules are of the form S[C[N 1 ]] → S[C[N 1 ]] and S[C[C 2 [N 2 ]]] → S 2 [C[C 2 [N 2 ]]] + M 2
, the first rule being (subst-r' ).

The two rules are of the form S[C[E[E

i [N i ]]]] → S i [C[E[E i [N i ]]]] + M i with E 1 = E 1 [.] E 2 [N 2 ][V] λ and E 2 = E 1 [N 1 ] E 2 [.][V] λ , N i → N i 5. The two rules are of the form S[C[E[N 1 ]]]] → S[C[E[N 1 ]] and S[C[E[E 2 [N 2 ]]]] → S 2 [C[E[E 2 [N 2 ]]]] + M 2
, with one of the following :

(a) N 1 = M [V] ↓ and the applied rule is (subst-r app ), (subst-r subst-r ) or (subst-r merge )

(b) N 1 = (P [U] ↑ ) E 2 [N 2 ][V] λ or N 1 = E 2 [N 2 ] (P [U] ↑ )[V] λ (c) N 1 = (E 2 [N 2 ][U] ↑ ) P [V] λ or N 1 = P (E 2 [N 2 ][U] ↑ )[V] λ (d) C = E = [.], N 1 = E 2 [N 2 ][V]
↑ and the first rule used is (subst-r' )

Proof. Lemma 4.1.13

We can write M in a unique way (modulo structual rules) as a sum of parallel of simple terms :

M = k M k , M k = i M i k •
The two reductions rules have a premise of the form S[N i ]. Identifying the terms of both sums, we can write

S 1 = [.] + k =k 1 M k and S 2 = [.] + k =k 2 M k . If k 1 = k 2 we are in the case (1), or S 1 = S 2 .
• If one of the rule used (let say the first one) is (subst-r' ), then

M k 1 = M k 1 [V] ↑ . Since M 1 = M 2
, the second rule can't be the same and is of the form

E[T ] → E[T ]
. This is the case (5d) of the lemma.

• Otherwise, the premises of the two rules have the form

S[C 1 [E 1 [P 1 ]]] → S[C 1 [E 1 [P 1 ]]] + M 1 and S[C 2 [E 2 [P 2 ]]] → S[C 2 [E 2 [P 2 ]]] + M 2 . If C 1 #C 2 ,
we are in case [START_REF] Accattoli | Proof nets and the call-by-value λ-calculus[END_REF]. If not, then either

C 1 = C 2 or C 2 = C 1 [C 2 ], C 2 = [.]
but the only rule that matches a parallel is (subst-r' ), and this is case [START_REF] Accattoli | A nonstandard standardization theorem[END_REF]. We assume from now on that C 1 = C 2 . We decompose E 1 and E 2 by their greatest common prefix, such that

E 1 = E[E 1 ] and E 2 = E[E 2 ]
with either

E 1 = E 2 = [.], or E 1 = [.], E 2 = [.], or E 1 #E 2 .
The former is excluded since the reducts N 1 and N 2 are assumed differents, and no rule have overlapping redex on base cases (when C and E are empty).

•

If E 1 #E 2 , since E 1 [P 1 ] = E 2 [P 2 ], then E 1 must be of the form E 1 R[V] λ , E 2 = L E 2 [V] λ with L = E 1 [P 1 ] and R = E 2 [P 2 ]
. This is case (4).

• Assume now that one of the two (let say E 1 ) is [.]. Then P 1 and E 2 have a common prefix. If P 1 is an application, it can't be the premise of the (β v ) rule with

P 1 = (λx.M ) V [U] λ , because then E 2 = E 2 V [U] λ or E 2 = (λx.M ) E 2 [U] λ but no non-empty context verifies E 2 [P 2 ] = V
for a value V . Thus it must be the premise of (subst-r' app ), and this corresponds to cases (5b) and (5c).

• If P 1 is not an application, since it must be both the premise of a rule and prefix of the context E 2 , the only remaining possibility is

P 1 = P 1 [V] ↓ .
Then P 1 can't be a value y, * , λy. or get(r), , [U] ↑ , because these constructors can't be in E 2 : we are in case (5a).

We can then proceed by case analysis to show weak confluence.

Proof. Proposition 4.1.12 We can write M, M 1 and M 2 in a unique way (modulo structual rules) as a sum of parallel of simple terms :

M = k M k , M 1 = k M 1 k , M 2 = k M 2 k
Let us examine all the possible cases of Lemma 4.1.13, assuming that N 1 = N 2 :

1. We have S 1 #S 2 , by identifying each terms, ∃k 1 = k 2 , S i = [.] + k =k i , and we have

M 1 = k =k 1 M k + N 1 + M 1 → k =k 1 ,k 2 M k + N 1 + N 2 + M 1 + M 2
as well as M 2 .

Let write

C i [N i ] = l∈L P l . Then there exists L 1 , L 2 ⊆ L. Since C 1 #C 2 , we have L 1 = L 2 and L 1 ⊆ L 2 and L 2 ⊆ L 1 , such that C i = [.] ( l∈L i P l )
and N i = l / ∈L i P l . The only rule that has a parallel of terms as premise is (subst-r' ). Thus L i are either singletons (if the corresponding rule is not (subst-r' )) or have size two. If they are disjoint, then L 2 ⊆ L \ L 1 and :

M 1 = S[N 1 ( l / ∈L 1 P l )] + M 1 = S[N 1 N 2 ( l / ∈L 1 ∪L 2 P l )] + M 1 → S[N 1 N 2 ( l / ∈L 1 ∪L 2 P l )] + M 1 + M 2 as do M 2 .
The only remaining case is if both rules are (subst-r' ) and

L 1 ∩ L 2 = {l 0 }. We write L 1 = {l 1 , l 0 }, L 2 = {l 2 , l 0 } and L = L \ {l 0 , l 1 , l 2 }. If P l 0 = P [V] ↑
is the "active" upward substitution in both reduction, we have

C 1 [N 1 ] = (P l 1 [V] ↓ P )[V] ↑ P l 2 ( l =L 3 P l ) → (P l 1 [V] ↓ P P l 2 [V] ↓ )[V] ↑ ( l =L 3 P l )
If P l 0 is the "passive" term in both reductions, with P l 1 = P l 1 [V] ↑ and

P l 2 = P l 2 [U] ↑ , then C 1 [N 1 ] = (P l 1 P l 0 [V] ↓ )[V] ↑ P l 2 [U] ↑ ( l =L 3 P l ) → * P l 1 (P l 0 [V] ↓ ) (P l 2 [U] ↑ [V] ↓ ) ( l =L 3 P l [V] ↓ ) → P l 1 (P l 0 [V] ↓ ) (P l 2 [V] ↓ [U] ↑ ) ( l =L 3 P l [V] ↓ ) → * (P l 1 [U] ↓ ) (P l 0 [W] ↓ ) (P l 2 [V] ↓ ) ( l =L 3 P l [W] ↓ )
using repeated (subst-r' ), (subst-r' ), (subst-r subst-r' ) and (subst-r merge ). Finally, if P l 0 is active in of the two (let say the first) and passive in the other, meaning that

P l 0 = P l 0 [V] ↑ , P l 2 = P l 2 [U] ↑ , then C 1 [N 1 ] = (P l 1 [V] ↓ P l 0 )[V] ↑ (P l 2 [U] ↑ ) ( l =L 3 P l ) → (P l 1 [V] ↓ P P l 2 [V] ↓ )[V] ↑ ( l =L 3 P l ) C 1 [N 1 ] = (P l 1 [V] ↓ P l 0 )[V] ↑ P l 2 [U] ↑ ( l =L 3 P l ) → * (P l 1 [V] ↓ ) P l 0 (P l 2 [U] ↑ [V] ↓ ) ( l =L 3 P l [V] ↓ ) → (P l 1 [V] ↓ ) P l 0 (P l 2 [V] ↓ [U] ↑ ) ( l =L 3 P l [V] ↓ ) → * (P l 1 [W] ↓ ) (P l 0 [U] ↓ ) (P l 2 [V] ↓ ) ( l =L 3 P l [W] ↓ )
On the other side,

C 2 [N 2 ] = P l 1 ((P l 0 [V] ↑ [U] ↓ ) P l 2 )[U] ↑ ( l =L 3 P l ) → * (P l 1 [U] ↓ ) (P l 0 [V] ↑ [U] ↓ ) P l 2 ( l =L 3 P l [U] ↓ ) → (P l 1 [U] ↓ ) (P l 0 [U] ↓ [V] ↑ ) P l 2 ( l =L 3 P l [U] ↓ ) → * (P l 1 [W] ↓ ) (P l 0 [U] ↓ ) (P l 2 [V] ↓ ) ( l =L 3 P l [W] ↓ ) 3. C 2 = Q[V] ↑ C 2 . Let write C = l P l and C 2 = [.] P . then C[N 1 ] = (Q (N 2 P )[V] ↓ )[V] ↑ . • Either N 2 = N 2 [U] ↑ Q and C[N 1 ] → * Q ((N 2 [U] ↑ ) Q )[V] ↓ ( l P l [V] ↓ ) → * Q (N 2 [V] ↓ [U] ↑ ) (Q [V] ↓ ) ( l P l [V] ↓ ) → * (Q[U] ↓ ) (N 2 [V] ↓ ) (Q [W] ↓ ) ( l P l [W] ↓ )
and

C[C 2 [N 2 ]] = (Q[V] ↑ ) (N 2 Q [U] ↓ )[U] ↑ ( l P l ) → * (Q[V] ↑ [U] ↓ ) N 2 (Q [U] ↓ ) ( l P l [U] ↓ ) → * (Q[U] ↓ ) (N 2 [V] ↓ ) (Q [W] ↓ ) ( l P l [W] ↓ ) • Otherwise, N 2 is a premise of the form E[Q ] and S[C[C 2 [E[Q ]]] → S[C[C 2 [E[Q ]]]] + M 2 . Then M 1 → * S[Q E[Q ][V] ↓ ( l P l [V] ↓ )] → S[Q E[Q ][V] ↓ ( l P l [V] ↓ )] + M 2
On the other side,

M 2 = S[(Q[V] ↑ ) E[Q ] ( l P l )] + M 2 → * S[Q (E[Q ][V] ↓ ) ( l P l [V] ↓ )] + M 2 4. S[C[E[E 1 [N 1 ]]]] + M 1 = S[C[E[E 1 [N 1 ] E 2 [N 2 ][V] λ ]]] + M 1 → S[C[E[E 1 [N 1 ] E 2 [N 2 ][V] λ ]]] + M 1 + M 2

(a)

The applied rule is either :

• (subst-r app ) and E 2 = E 2 Q[U] λ or E 2 = Q E 2 [U] λ • (subst-r subst-r'
) and

E 2 = E 2 [U] ↑ • (subst-r merge ) and E 2 = E 2 [V] ↓
In the three cases, it is clear that the reductions are independant : the first one can be performed in M 2 and vice-versa to get a common reduct.

The same argument applies to the other four cases.

Preorder on terms

In the coming Section 4.4 and Section 4.3, we will need to compare the possible behaviors of similar terms. For example, take a term M [U, V] ↓ that is strongly normalizing. Intuitively, if we remove available reference bindings to form

M [U] ↓ or M [V]
↓ , the result should also be strongly normalizing: removing available substitutions may only restrict the possible behaviors. The aim of this subsection is formalize this relation between terms of "being similar but able to do more", and to prove the kind of statement about termination we just made above.

To do so, we introduce the preorder (and an indexed family V of preorders), where M N means that the two terms are essentially the same, but N may have more available reference substitutions and possibly in different positions. For example, this is typically the case if N is a reduct of M [V] ↓ using only downward structural rules. This preorder encompasses the notion of possible behaviors: M N means that everything that can be done by M can be done by N . This is the substance of Proposition 4.1.18. Definition 4.1.14. Reachability and Associated Preorder Let M be a term, and N an occurrence of a subterm in M that is not under an abstraction. We define Reach(N, M ), a reference substitution, as the merge of all substitutions that are in scope of this subterm in M , as follows. Recall Notation 4.1.5.

• If M = N then Reach(N, M ) is nowhere defined.

• If M = M [U] ↓ then Reach(N, M ) = U, Reach(N, M
), the juxtaposition of U and Reach(N, M ).

• If M = M [σ] then Reach(N, M ) = Reach(N, M ){σ}.
Lemma 4.1.17. Invariance by (subst-r) reductions Let M N (resp. M V N ).

• If M → M by a (subst-r) rule except (subst-r get ) then M N (resp. M V N )

• If N → N by a (subst-r) by a (subst-r) rule except (subst-r get ) then M N (resp. M V N ).

Proof. Lemma 4.1.17 Clearly, a (subst-r) rule does not modify the skeleton, so Sk(M ) = Sk(M ) = Sk(N ). It is also almost immediate to see that the rules that propagate reference substitutions, or the (subst-r val ) rule that erases a substitution that is only in the scope of a value, do not modify the reachability sets of an occurrence of get(r) or

M = M 1 M 2 [V] λ in M .
This is the main technical result on the preorders:

Proposition 4.1.18. Simulation preorder Let M N (resp. M V N ). If M → M then ∃n ≥ 0, N → n N with M N (resp. M V N ). If the applied rule is not a (subst-r) or is (subst-r get ), then n > 0.
From this, we deduce the important properties of the preorders: 1. If M N , then if N is strongly normalizing, so is M .

2. If M N , then M is strongly normalizing if and only if N is.

Proof. Corollary 4.1.19 Let M N , assume that M has an infinite reduction sequence. We can map this sequence to (finite or infinite) sequence N → * N 1 → * N 2 . . . by 4.1.18. As (subst-r) rules alone without (subst-r get ) are strongly normalizing, this means that the infinite reduction sequence of M must contain an infinite number of steps that are not (subst-r) rules or are a (subst-r get ). But then, as such steps are simulated by at least one step in the sequence N → * N 1 → * . . ., the latter must be infinite. This contradicts the fact that N is strongly normalizing. Thus M has no infinite reduction sequence. To do so, we just apply the rule (subst-r ) until it is not possible anymore to get N → * C[N ]. Then, E[P ] and N having the same skeleton, N can be written as E [P ] where E is E with additional references substitutions, and P and P have the same skeleton and the same head constructor. Indeed, if P would have additional substitutions in head position we could always include them in E : in fact we take the maximal E that satisfies the previous decomposition.

Note that the reachability sets of subterms in C (respectively E,E ) only depends on C (resp. C, E and C, E ). On the other side, the reachability sets of subterms in P (resp. P ) are unions of substitutions occurring in P, E (resp. P , E ) and C.

• If the reduction rule is one of the (subst-r) except (subst-r get ), by Lemma 4.1.17, n = 0 works.

• (subst-r get ) :

P = get(r)[V] ↓ → V ∈ V(r) and P = get(r)[V ] ↓ . V(r) is in Reach(get(r), N
), so by iterated application of (subst-r) rules except (subst-r get ) and (subst-r val ), we can push (without modifying the skeleton nor the reachability sets) the corresponding substitutions down until it reaches get(r) in P . Then, we can perform a (subst-r get ) reduction. All the other reachability sets of gets or application are left unmodified.

• (β v ) : P = (λx.Q) V [V] λ → T = Q[x/V ][V] ↓ . Up to (subst-r val ) re- ductions, P = (λx.Q) V [V ] λ → T = Q[x/V ][V ] ↓ .
The condition on reachabiliy sets for application in the defintion of precisely ensures that all the gets and applications in Q have the same reachability in

C[E[T ]] and in C[E [T ]].
(subst) rules

• (subst var ) : P = x[σ] → x or σ(x), and P = x[V] ↓ [σ] → x[σ] → x or σ(x).
• (subst app ) :

P = Q 1 Q 2 [V] λ [σ] → T = (Q 1 [σ]) (Q 2 [σ])[(V [σ])] λ . We have P = (Q 1 [U] λ ) (Q 2 [W] λ )[V ] λ [σ] → * (Q 1 [σ][U [σ]] ↓ ) (Q 2 [σ][V [t]W ] ↓ )[V [σ]] λ .
By definition of reachability sets, they are invariant by all the rule applied.

• We proceed the same way for other cases : the var substitution just go through the additionnal references substitutions, and by design, reachability sets are not modified.

(subst-r') rules

• Upward substitutions commute with downward ones without interacting. On the other hand, they can span new downward substitutions but in this case, they do it in the same way for both P and P and thus do not modify the inclusion relation on reachability sets.

Stratification and Type System

We present in this section a stratified type and effect system for λ cES inspired from [START_REF] Amadio | On stratified regions[END_REF][START_REF] Madet | Complexité Implicite de Lambda-Calculs Concurrents[END_REF]. A type and effect system aims at statically track the potential effects that a term can produce when reduced. Here, the considered effects are read from or write to references.

The Type System of λ cES

Formally, the type and effect system is defined as follows.

-effects e, e ⊂ {r 1 , r 2 , . . .} -types

α ::= B | A -value types A ::= Unit | A e → α | Ref r A
The type Unit is the type of * . The function type A e → α is annotated with an effect e: the set of references the function is allowed to use. Finally, the type Ref r A states that the reference r can only be substituted with values of type A. Since thread cannot be fed as an argument to a function, the type of the parallel components of a program is irrelevant. They are given the opaque behavior type B. We separate α-types and A-types to ensure that B cannot be in the domain of a function.

In the typing rules we use two distinct contexts: variable contexts Γ of the form x 1 : A 1 , . . . , x n : A n and reference contexts R of the form r 1 : A 1 , . . . , r n : A n . The latter indicates the type of the values that a reference r appearing in M can hold. If the order of variables in Γ is irrelevant, the order of references in R is important.

In order to ensure termination, the type and effect system is stratified: this stratification induces an order forbidding circularity in reference assignments. It is presented as a set of rules to build the reference context and can be found in Figure 4.1. It states that when a new reference is added to the context, all references appearing in its type must already be in R. In Figure 4.1 the entailment symbol ( ) is overloaded with several meanings: • R is well formed, written R , means that the references appearing in R are stratified.

∅ R A r / ∈ dom(R) R, r : A R R Unit R R B R A R α e ⊆ dom(R) R A e → α R r : A ∈ R R Ref r A
• A type α is well formed under R, written R (α, e), means that all references appearing in e and α are in R.

• A variable context Γ is well formed under R, written R Γ, means that all the types appearing in Γ are well formed under R.

The type and effect system features a subtyping relation whose definition rules are presented in Figure 4.2. It formalizes the idea that a function of type A {r} → α is not obliged to use the reference r. Typing judgments overload once more the symbol ( ) and take the form R; Γ M : (α, e) where R is the reference context, Γ the variable context, α the type of M and e the references that M may affect. Using the stratification and the subtyping relation, the typing rules for the language λ cES are presented in Figure 4.3. For succinctness, the application rule has been factorized into two rules, (APP) and (SUBST) for ξ = λ. Thus (APP) is not a legitimate rule but an abuse of notation, and must be followed by an appropriate (SUBST) in any type derivation. Remark 4.2.1. In Rule (lam), when abstracting over a variable in a term R; Γ, x : A M : (α, e), the resulting value λx.M is pure and hence its effects should be the empty set. However one must remember that the body of this abstraction is potentially effectful: this is denoted by annotating the functional arrow "→" with a superscript indicating these effects. Also note that in general, the order of references in R is capital: it is the order induced by stratification.

Let (α, e) be a type and effect well-formed under a reference context R, i.e. R (α, e). We give two definitions that allow to refer to the effects contained implicitly or explicitly in (α, e). Eff R (α, e) represents the effects of e together with the effects placed on the arrows of α. Reg R (α, e), includes not only Eff R (α, e) but also all the effects involved in the judgement R (α, e). Definition 4.2.2. Effect of a type and effect Let R (α, e). We define the effect Eff R (α) as:

R α ≤ α (ref ) e ⊂ e ⊂ dom(R) R α ≤ α R (α, e) ≤ (α , e ) (cont) R A ≤ A R (α, e) ≤ (α , e ) R A e → α ≤ A e → α (arrow) Figure 4.2: Subtyping relation R Γ, x : A R; Γ, x : A x : (A, ∅) (var) R Γ R; Γ * : (Unit, ∅) (unit) R Γ r : A ∈ R R; Γ r : Ref r A (reg) R; Γ, x : A M : (α, e) R; Γ λx.M : (A e → α, ∅) (lam) R; Γ M : (A e 1 → α, e 2 ) R; Γ N : (A, e 3 ) R; Γ M N : (α, e 1 ∪ e 2 ∪ e 3 ) (app) R; Γ r : Ref r A R; Γ get(r) : (A, {r}) (get) R; Γ M : (α, e) R (α, e) ≤ (α , e ) R; Γ M : (α , e ) (sub) R; Γ, x 1 : A 1 , . . . , x n : A n M : (α, e) ∀i : R; Γ V i : (A i , ∅) R; Γ M [∀i : x i → V i ] : (α, e) (subst) ∀i : R; Γ r i : Ref r i A i R; Γ M : (α, e) ∀i : r i ∈ e ∀i : V ∈ E i =⇒ R; Γ V : (A i , ∅) R; Γ M [∀i : r i → E i ] ξ : (α, e) for ξ ∈ {↑, ↓, λ} (subst-r) i = 1, 2 R; Γ M i : (α i , e i ) R; Γ M 1 M 2 : (B, e 1 ∪ e 2 ) (par) i = 1, 2 R; Γ M i : (α, e) R; Γ M 1 + M 2 : (α, e) (sum)
Eff R (Unit) = ∅ Eff R (B) = ∅ Eff R (A e → α) = Eff R (A) ∪ Eff R (α) ∪ e We define Eff R (α, e) = Eff R (α) ∪ e.
Definition 4.2.3. Region of a type and effect Let R (α, e). We define the set Reg R (α) as:

Variables substitutions • (subst var ) We have R; Γ σ(x i ) : (A i , ∅) R; Γ y : (B, ∅) (var) R; Γ y[σ] : (B, ∅) (subst)
with Γ = Γ, x 1 : A 1 , . . . , x n : A n if i ranges over 1 . . . n. We have

R; Γ y : (B, ∅) (var) if σ is undefined at y or R; Γ σ(y) : (A i 0 , ∅) if ∃i 0 , x i 0 = y and thus A i 0 = B.
• (subst unit ) : just apply the (unit) typing rule.

• (subst app ) R; Γ r i : Reg r i A i ∀V ∈ V(r i ) : R; Γ V : (A i , ∅) R; Γ M : (C e 1 → α, e 2 ) R; Γ N : (C, e 3 ) R; Γ M N : (α, e) (app) R; Γ M N [V] λ (subst-r) (subst) R; Γ σ(x j ) : (B j , ∅) R; Γ M N [V] λ R; Γ M N [V] λ [σ] : (α, e)
With Γ = Γ, x 1 : A 1 , . . . , x n : A n and e 1 ∪ e 2 ∪ e 3 = e. We can derive

(subst) R; Γ σ(x j ) : (B j , ∅) R; Γ M : (C e 1 → α, e 2 ) R; Γ M [σ] : (C e 1 → α, e 2 ) R; Γ σ(x j ) : (B j , ∅) R; Γ N : (C, e 3 ) R; Γ N [σ] : (C, e 3 ) (subst) R; Γ (M [σ]) (N [σ]) : (α, e) (app)
For any V ∈ V(r i ), one has

R; Γ σ(x j ) : (B j , ∅) R; Γ V : (A i , ∅) R; Γ V [σ] : (A i , ∅) (subst)
And finally

R; Γ P : (α, e) R; Γ r i : Reg r i A i ∀V ∈ V(r i ) : R; Γ V [σ] : (A i , ∅) R; Γ (M [σ]) (N [σ])[V[σ]] λ (subst-r) • (subst λ ) : R; Γ σ(x i ) : (A i , ∅) R; Γ , y : A M : (α, e) R; Γ λy.M : (A e → α, ∅) (lam) R; Γ λy.M [σ] : (A e → α, ∅) (subst)
then we just swap the two rules :

(weak) R; Γ σ(x i ) : (A i , ∅) R; Γ, y : A σ(x i ) : (A i , ∅) R; Γ , y : A M : (α, e) R; Γ, y : A M [σ] : (α, ∅) (subst) R; Γ λy.(M [σ]) : (A e → α, ∅) (lam)
• (subst get ) :

R; Γ σ(x i ) : (A i , ∅) R; Γ r : Reg r B R; Γ get(r) : (B, {r}) (get) R; Γ get(r)[σ] : (B, {r}) (subst)
We can juste recast the get rule without the weakened x i s :

R; Γ r : Reg r B R; Γ get(r) : (B, {r}) (get)
• (subst ) :

R; Γ σ(x j ) : (A j , ∅) i = 1, 2 R; Γ M i : (α i , e i ) R; Γ M 1 M 2 : (B, e) (par)
R; Γ M 1 M 2 [σ] : (B, e) (subst)
Then i = 1, 2 R; Γ σ(x j ) : (A j , ∅) R; Γ M i : (α i , e i ) R; Γ M i [σ] : (α i , e i ) (subst) R; Γ (M 1 [σ]) (M 2 [σ]) : (B, e) (par)
• (subst subst-r ) :

R; Γ σ(x j ) : (A j , ∅) R; Γ r i : Reg r i A i ∀U ∈ U(r i ) : R; Γ U : (A i , ∅) R; Γ M : (α, e) R; Γ M [U] ↓ : (α, e) (subst-r) R; Γ M [U] ↓ [σ] : (α, e) (subst)
Then for any

U ∈ U(r i ) R; Γ U : (A i , ∅) R; Γ U [σ] : (A i , ∅) (subst) It follows R; Γ r i : Reg r i A i ∀U ∈ U(r i ) : R; Γ U : (A i , ∅) R; Γ σ(x j ) : (A j , ∅) R; Γ M : (α, e) R; Γ :[σ/M ](α, e) (subst) R; Γ M [σ][U[σ]] ↓ : (α, e) (subst-r)
• (subst subst-r ) : exactly as the previous case (the typing rules and reduction rules being similar)

• (subst merge ) We need a simple substitution lemma to handle this case of the meta substitution. Let Γ I = • i∈I x i : A i and Γ J = • j∈J x j : A j where • is the list concatenation.

∀U ∈ U(r j ) : R; Γ U : (A j , ∅)

∀V ∈ V(r i ) : R; Γ, Γ J V : (A i , ∅) R; Γ, Γ J , Γ I M : (α, e) R; Γ J M [(x i )/(V i )] : (α, e) (subst) R; Γ M [(x i )/(U i )][(y j )/(U j )] : (α, e) (subst)
Then we have

∀V ∈ V i : R; Γ V {(U j )/(y j )} : (A i , ∅) ∀U ∈ U j : R; Γ U : (A j , ∅) R; Γ, Γ J , Γ I M : (α, e) R; Γ M [(z i )/(W i )] : (α, e) (subst)
Downward references substitutions

• (subst-r val ) R; Γ r i : Reg r i A i ∀U ∈ U(r i ) : R; Γ U : (A i , ∅) R; Γ V : (A, ∅) R; Γ V : (A, {r}) (sub) R; Γ V [U] ↓ : (A, e) (subst-r)
Then we just reuse the typing derivation of

R; Γ V : (A, ∅) R; Γ V : (A, {r}) (sub)
• (subst-r )

R; Γ r i : Reg r i A i ∀U ∈ U(r i ) : R; Γ U : (A i , ∅) R; Γ M i : (α i , e i ) R; Γ M 1 M 2 : (B, e) (par) R; Γ M 1 M 2 [U] ↓ : (B, e) (subst-r)
Then we commute the two rules

R; Γ r i : Reg r i A i ∀U ∈ U(r i ) : R; Γ U : (A i , ∅) R; Γ M i : (α i , e) R; Γ M i [U] ↓ : (α i , e) (subst-r) R; Γ (M 1 [U] ↓ ) (M 2 [U] ↓ ) : (B, e) (par)
• (subst-r subst-r' )

R; Γ r i : Reg r i A i ∀V ∈ V(r i ) : R; Γ V : (A i , ∅) R; Γ M : (α, e) R; Γ M [V] ↑ : (α, e) (subst-r) R; Γ r j : Reg r j B j ∀U ∈ U(r j ) : R; Γ U : (B j , ∅) R; Γ M [V] ↓ : (α, e) R; Γ M [V] ↑ [U] ↓ : (α, e) (subst-r)
We just swap the two rules

R; Γ r j : Reg r j B j ∀U ∈ U(r j ) : R; Γ U : (B j , ∅) R; Γ M : (α, e) R; Γ M [U] ↓ : (α, e) (subst-r) R; Γ r i : Reg r i A i ∀V ∈ V(r i ) : R; Γ V : (A i , ∅) R; Γ M [U] ↓ : (α, e) R; Γ M [U] ↓ [V] ↑ : (α, e) (subst-r) • (subst-r-merge) R; Γ r i : Reg r i A i ∀V ∈ V(r i ) : R; Γ V : (A i , ∅) R; Γ M : (α, e) R; Γ M [V] ↓ : (α, e) (subst-r) R; Γ r j : Reg r j B j ∀U ∈ U(r j ) : R; Γ U : (B j , ∅) R; Γ M [V] ↓ : (α, e) R; Γ M [V] ↓ [U] ↓ : (α, e) (subst-r)
Then we have

R; Γ r k : Reg r k A k ∀W ∈ (U + V)(x k ) : R; Γ W : (A k , ∅) R; Γ M : (α, e) R; Γ M [V, U] ↓ : (α, e) (subst-r) • (subst-r-app) R; Γ r i : Reg r i A i ∀V ∈ V(r i ) : R; Γ V : (A i , ∅) R; Γ M : (A e 1 → α, e 2 ) R; Γ N : (A, e 3 ) R; Γ M N : (α, e) (app) R; Γ M N [V] λ : (α, e) (subst-r) R; Γ r j : Reg r j B j ∀U ∈ U(r j ) : R; Γ U : (B j , ∅) R; Γ M N [V] λ : (α, e) R; Γ M N [V] λ [U] ↓ : (α, e) (subst-r)
That we can turn into

R; Γ r j : Reg r j B j ∀U ∈ U(r j ) : R; Γ U : (B j , ∅) R; Γ M : (A e 1 → α, e 2 ) R; Γ M [U] ↓ : (A e 1 → α, e 2 ) (subst-r) R; Γ r j : Reg r j B j ∀U ∈ U(r j ) : R; Γ U : (B j , ∅) R; Γ N : (A, e 3 ) R; Γ N [U] ↓ : (A, e 3 ) (subst-r) R; Γ M [U] ↓ : (A e 1 → α, e 2 ) R; Γ N [U] ↓ : (A, e 3 ) R; Γ (M [U] ↓ ) (N [U] ↓ ) : (α, e) (app) R; Γ r k : Reg r k A k ∀W ∈ (V + U)(r i ) : R; Γ W : (C i , ∅) R; Γ (M [U] ↓ ) (N [U] ↓ ) : (α, e) R; Γ (M [U] ↓ ) (N [U] ↓ )[W] λ (subst-r) • (subst-r get ) Write S = M 1 + . . . + M n + [],
with n ≥ 0. The derivation tree of

P = C[E[get(r)[V] ↓ ]] is of the form R; Γ r i : Reg r i A i ∀V ∈ V(r i ) : R; Γ V : (A i , ∅) R; Γ get(r) : (A, e) R; Γ get(r)[V] ↓ : (A, e) (subst)
[. . .] R; Γ P : (α, e )

And of the full term :

(∀i : 1 ≤ i ≤ n) R; Γ M i : (α, e ) R; Γ P : (α, e ) R; Γ S[P ] : (α, e ) (sum)
To get the first term of the reduct, we just remove the subst rule :

(∀i : 1 ≤ i ≤ n) R; Γ M i : (α, e ) R; Γ get(r) : (A, e) [. . .] R; Γ C[E[get(r)]] : (α, e ) R; Γ S[C[E[get(r)]]] : (α, e ) (sum)
Now if V is undefined at r we are done. Otherwise, we substitute get(r) by a value V ∈ V(r) :

R; Γ V : (A, ∅) R; Γ V : (A, e) (sub)
[. . .] R; Γ C[E[V ]] : (α, e )
And we can finally derive

∀V ∈ V i 0 : R; Γ C[E[V ]] : (α, e ) R; Γ S[C[E[get(r)]]] : (α, e ) R; Γ S[C[E[get(r)]]] + V ∈V(r) C[E[V ]] : (α, e ) (sum)
Upward references substitutions

• (subst-r' ) R; Γ M : (α 1 , e 1 ) R; Γ r i : Reg r i A i ∀V ∈ V(r i ) : R; Γ V : (A i , ∅) R; Γ N : (α 2 , e 2 ) R; Γ N [V] ↑ : (α 2 , e 2 ) (subst-r) R; Γ M (N [V] ↑ ) : (B, e) (par)
Then we have

(subst-r) R; Γ r i : Reg r i A i ∀V ∈ V(r i ) : R; Γ V : (A i , ∅) R; Γ M : (α 1 , e 1 ) R; Γ (M [V] ↓ ) : (α 1 , e 2 ) R; Γ N : (α 2 , e 2 ) R; Γ (M [V] ↓ ) N : (B, e) (par)
R; Γ r i : Reg

r i A i ∀V ∈ V(r i ) : R; Γ V i : (A i , ∅) R; Γ (M [V] ↓ ) N : (B, e) R; Γ (M [V] ↓ ) N [V] ↑ : (B, e) (subst-r) • (subst-r' app-left ) R; Γ r i : Reg r i A i ∀V ∈ V(r i ) : R; Γ V : (A i , ∅) R; Γ M : (A e 2 → α, e 3 ) R; Γ M [V] ↑ : (A e 2 → α, e 3 ) (subst-r) R; Γ (M [V] ↑ ) : (B e 1 → α, e 2 ) R; Γ N : (A, e 3 ) R; Γ (M [V] ↑ ) N : (α, e) (app)
R; Γ r j : Reg r j B j ∀U ∈ U(r j ) : R;

Γ U : (B j , ∅) R; Γ (M [V] ↑ ) N : (α, e) R; Γ (M [V] ↑ ) N [U] λ : (α, e) (subst-r)
That we turn to

R; Γ M : (A e 1 → α, e 2 ) R; Γ r i : Reg r i A i ∀V ∈ V(r i ) : R; Γ V : (A i , ∅) R; Γ N : (A, e 3 ) R; Γ N [V] ↓ : (A, e 3 ) (subst-r) R; Γ M (N [V] ↓ ) : (α, e) (app) R; Γ r k : Reg r k C k ∀W ∈ (V + U)(r k ) : R; Γ W : (C k , ∅) R; Γ M (N [U, V] ↓ ) : (α, e) R; Γ M (N [V] ↓ )[U, V] λ : (α, e) (subt-r) R; Γ r k : Reg r k C k ∀W ∈ (U + V)(r k ) : R; Γ W : (C k , ∅) R; Γ M (N [V] ↓ )[U, V] λ : (α, e) R; Γ M (N [V] ↓ )[U, V] λ [V] ↑ : (α, e) (subst-r)
• (subst-r' app-right ) : same as (subst-r' app-left )

• (subst-r' ) Assume that S = M 1 + . . . + M n + [],
with n ≥ 0, then we have → α is to be an abstraction, but then M would reduce by (β v ). Thus one of them is of the form M norm and so is M .

R; Γ r j : Reg r j A j ∀V ∈ V(r j ) : R; Γ V : (A j , ∅) R; Γ M : (α, e) R; Γ M [V] ↑ : (α, e) (subst-r) (∀i : 1 ≤ i ≤ n) R; Γ M i : (α, e) R; Γ M [V] ↑ : (α, e) R; Γ S[M [V] ↑ ] : (α, e) (sum) if Q = Q [V] ↑ .
• if M = M [V]
↑ then it reduces by (subst-r' ).

• if M = P Q, assume that P → P by any rule excepted (subst-r' ), then so would M , taking E = [.] and C = [.] Q. The same holds for Q.

Now, if P or Q is of the form P [V]
↑ , then M reduces by (subst-r' ). Thus P and Q does not reduce, and by induction, are of the form i M i with M i a value or of the form M norm , hence so is M .

Finally, if M = M i , then M is normal if and only if each M i is and the induction hypothesis immediately gives the result.

Termination

Our main result is a finitary, interactive proof of strong normalization for λ cES . This section is devoted to the presentation of the problem in the context of references, the explanation of why the existing solutions do not apply to our setting and what we propose instead.

Shortcoming of Existing Solutions Introduced by Tait in 1967 [START_REF] Tait | Intensional interpretations of functionals of finite type[END_REF], reducibility is a widely used, versatile technique for proving strong normalization of lambdacalculi. The core of this technique is to define inductively on types τ a set SC(τ ) of well typed terms, called strongly computable terms, satisfying a series of properties. One proves that terms in SC(τ ) are strongly normalizing (Adequacy) and (the most difficult part) that all well typed terms of a type τ are actually in SC(τ ).

When adapting this technique to a type and effect system, the main difficulty is that the definition is not obviously inductive anymore. To define SC(A e → α), we need to have defined the types of references appearing in e. But e can itself contain a reference of type A e → α: in the Landin's fixpoint example shown in the introduction of this chapter, the looping term has the type Unit {r} → Unit while r has the same type. The role of stratification is to induce a well-founded ordering on types so that the definition becomes consistent.

The solution offered by stratification of the type system is however not enough for λ cES . In Boudol [START_REF] Boudol | Typing termination in a higher-order concurrent imperative language[END_REF], where the technique is introduced, concurrency is explicitly controlled by threads themselves that are guaranteed to be the only process in execution during each slice of execution. In λ cES , reduction steps are performed in arbitrary threads such that stores may be affected by others between two atomic steps in a particular thread.

To overcome this issue, for the language presented in Section 4.4.1, Amadio [START_REF] Amadio | On stratified regions[END_REF] strengthens the condition defining SC sets by asking that they also terminate under infinite stores of the form (r ⇐ V 1 . . . r ⇐ V n . . .) with (V i ) an enumeration of all the elements of SC(α). In this setting, infinite stores are static top-level constructions: once saturated, they are invariant by any new assignment. In a term (M 1 M 2 S) with S being such a store, any memory operation of M 2 is completely invisible to M 1 and one can prove separately the termination of each thread.

However, this solution is not easily transposable to λ cES . First of all, the rule (subst-r get ) produces all the possible values associated to a store. The corresponding get(r)[V] ↓ would reduce to an infinite sum get(r) + i V i where, even if each summand terminates, there is also for any positive integer n a summand that takes at least n steps to reach normal form. The total sum is not terminating anymore. Secondly, unlike static top-level stores, reference substitutions are duplicated, erased and exchanged in an interactive way between threads.

Our Solution To prove strong normalization of λ cES , we change gears. With explicit substitutions, assignments and reads are a way of exchanging messages between threads or subterms. Apart from the termination of each term in isolation, the key property we need is that threads cannot exchange an infinite amount of messages.

We formalize this condition by strengthening the definition of strongly computable terms. We force them to also be well-behaved. A well-behaved term must only emit a finite number of upward substitutions containing strongly computable terms when placed in a "fair" context. A fair context is a context that would only send strongly computable reference substitutions (albeit potentially infinitely many).

These notions are defined in Section 4.3.1, while the strong normalization result is spelled out in Section 4.3.2.

Technical Definitions

Remark 4.3.1. In the following, we do not want to deal with the clumsiness of handling sums of terms everywhere. If a reduction sequence is seen as a tree, where branching points correspond to (subst-r get ) and the children to all the summands produced by this rule, then by König's lemma it is finite if and only if all its branches are finite. We will thus use the alternative non-deterministic reduction → nd (Definition 4.1.9), such that a sequence of reductions → nd corresponds to a branch in the original reduction system. Proving the termination of → nd is then sufficient, thanks to the König's lemma. In the rest of the chapter, we only consider simple terms (non-sums) and the → nd reduction, that we will just write →.

The purpose of the following Definition 4.3.2 is to formalize the interaction of a subterm with its context as a play against an opponent that can non-deterministically drop downward substitutions at the top level or absorb upcoming substitutions. This is summarized in the condition (WB) of Definition 4.3.5. Definition 4.3.2. Environment Reduction Let M : (α, e) be a well typed term. Let (V i ) be a sequence of reference substitutions such that M [V i ] ↓ is well typed that we write (M, (V i )). We call a (M, (V i ))-reduction a finite or infinite reduction sequence starting from M where each step is either a → nd , or an interaction with the environment defined by the additional rules

M [V] ↑ → ↑ M and M → ↓ M [V i ] ↓ .
The sets of strongly computable terms are defined by induction on a pair (α, e) of type and effect, with respect to the following well-founded ordering introduced in [START_REF] Boudol | Typing termination in a higher-order concurrent imperative language[END_REF]:

Definition 4.3.

Type and effect ordering

We define the size of a type |α| by:

|Unit| = 1 |B| = 1 |A e → α| = |A| + |α| + 1
For two types and effect (α 1 , e 1 ) and (α 2 , e 2 ) such that R (α 1 , e 1 ) and R (α 2 , e 2 ), (α 1 , e 1 ) ≺ R (α 2 , e 2 ) if and only if: [START_REF] Boudol | Typing termination in a higher-order concurrent imperative language[END_REF]Boudol] Well-ordering of type and effect The ≺ R order is well-founded, that is there is no infinite sequence (α i , e i ) i∈N with ∀i ∈ N, (α i+1 , e i+1 ) ≺ R (α i , e i ).

1. Reg R (α 1 , e 1 ) Reg R (α 2 , e 2 ), or 2. Reg R (α 1 , e 1 ) = Reg R (α 2 , e 2 ) and |α 1 | < |α 2 | Proposition 4.3.4.
We can now define the notion of strongly computable terms as follows, by induction with respect to the ≺ R order. Definition 4.3.5. Strongly Computable Terms The set SC R (α, e) of strongly computable terms of type (α, e) is defined as follows:

Base type. Assume that α = Unit | B. Then M ∈ SC R (α, e) if it is well-typed R M : (α, e)
(SN) Strongly normalizing under reference substitutions: For all V verifying ∀r, V(r) defined =⇒ r ∈ e, V(r) ⊆ SC R (R(r), ∅), the term M [V] ↓ is strongly normalizing.

(WB) Well Behaved: For any (V i ) such that (M, (V i )) and verifying ∀i, ∀r, V i (r) defined r ∈ e, V i (r) ⊆ SC R (R(r), ∅) , for any (M, (V i ))-reduction M = M 0 → . . . → M n → . . ., there exists n 0 ≥ 1 such that for all k ≥ 1:

1. If M k-1 is of the form N [U] ↑ with M k-1 → ↑ M k then ∀r, U(r) defined =⇒ U ⊆ SC R (R(r), ∅), 2. If k ≥ n 0 then M k-1 → M k is not a (→ ↑ ) step.
Inductive case. M belongs to SC R (A

e 1 → α, e) provided that R M : (A e 1
→ α, e). Then for all V ∈ SC R (A, ∅), we have M V ∈ SC R (α, e ∪ e 1 ). Notation 4.3.6. By abuse of notation, we shall omit in the following one or more of the R, α, e when it is obvious from the context and just write M ∈ SC. Moreover, we also write V ⊆ SC to mean that for all r for which V is defined, we have V(r) ⊆ SC R (R(r), ∅). Remark 4.3.7. The condition (SN) requires terms to be strongly normalizing when put under any finite reference substitution of strongly computable terms. The finiteness is sufficient, thanks to the presence of condition (WB). This rather technical condition is the well-behaved requirement: it says that there are at most n 0 (→ ↑ ) steps.

Strong Normalization for λ cES

We are now ready to state and sketch the proof of strong-normalization for λ cES . The easy part is the adequacy result, stated as follows.

Lemma 4.3.8. Adequacy If M ∈ SC(α, e) then M is strongly normalizable.

Proof. Lemma 4.3.8 We will prove additionally by induction on types that for any value type A, there exists V α ∈ SC(A, ∅).

• For α = Unit | B, if M ∈ SC(α, f ) did not terminate, then neither would M [V] ↓ . If α = Unit, then * ∈ SC(Unit, ∅) is a value populating SC(α, ∅). • For α = A e 1 → α , if M ∈ SC(α, e ) did
not terminate, neither would M V for V ∈ SC(A, ∅), which exists since the latter set is not empty by induction hypothesis. For V α ∈ SC(α , ∅), then λx.V α is a value populating SC(α, ∅)

The heart of our result is the opposite result, the soundness: Proposition 4.3.9. Soundness Let R; x 1 : A 1 , . . . , x n : A n P : (α, e). Let σ be a variable substitution with dom(σ) ⊆ {x 1 , . . . , x n } and ∀x ∈ dom(σ), σ(x)

∈ SC R (A i , ∅). Then P [σ] ∈ SC R (α, e).
The proof of Proposition 4.3.9 is rather technical and require the introduction of auxiliary lemmas to be worked out. We first give a high-level sketch of some representative cases first, to focus on the important ideas and intuitions. The reader may refer to Section 4.3.3 for a complete proof.

Sketch of the proof of Proposition 4.3.9. The proof is performed by induction on the structure of the term P . To show how the proof works, we focus on two representative cases, the abstraction and the parallel composition.

Abstraction Let us treat the case P = λx.M with R, x : A 1 λx.M : (α, e 1 ). By induction, for any

V ∈ SC R (A 1 , ∅), e ⊇ e 1 , M [x → V ] ∈ SC R (α, e ). For e ⊆ dom(R), we want to show that P ∈ SC R (A 1 e 1 → α, e). Let α = A 2 e 2 → . . . e n-1 → A n e n
→ β be the expansion of the type of P , where β is either Unit or B. If we unfold the recursive definition of SC sets, proving that P ∈ SC(α) amounts to check that Λ(P, U, (N i )) := P V 1 . . . V n [U] ↓ satisfies (SN) and (WB) for all strongly computable V 1 , . . . , V n and U with suitable types.

While each M i do terminate in isolation as strongly computable terms, the possibility of an infinite exchange of substitutions prevent us from using (SN) directly to deduce the strong normalization of P . This is the precise role of (WB): the sequence of reductions from M k i to M k+1 i inside its context can be mapped to an environment reduction of M i . The environment abstracts the role of the adverse thread M 1-i which can generate new downward reference substitutions at the top level. We adopt the following strategy :

1. Use (WB) to show that the exchange of substitutions between the two threads M 1 and M 2 must come to an end, and that all the exchanged substitutions are strongly computable.

2.

For each M i , gather all the substitutions (a finite number according the previous step) it receives during the reduction of Λ and merge them into one substitution X i 3. Show that after a finite number k of steps, when the two threads do not exchange reference substitutions anymore, we can bound each reduct

M k i inside Λ by a reduct of M i [X ] ↓ .
Since the bounding terms are strongly normalizing by (SN), so are the M k i s by Proposition 4.1.18, and the reduction of Λ must be finite from this point.

Putting together Proposition 4.3.9 (with n = 0) and Lemma 4.3.8, we can easily prove the strong normalization result for λ cES . 1. Consider Λ(M, U, (U i )) for appropriate U and (U i ) (as given in Lemma 4.3.12).

The possible immediate reducts of Λ may have the following form:

(a) M V 1 . . . V n-1 [V] λ (V n [V] ↓ ) if the substitution is pushed down (b) M V 1 . . . V n [V] ↓ with M → M if a reduction happens inside M (c) N V 2 . . . V n [V] ↓ if M = λx.M interacts with V 1 by a β V reduction.
As each V i is inert, and propagating of reference substitutions is a terminating process, an infinite reduction sequence of Λ must at some point either reduce inside M as in (b), propagate the substitution V in M or perform a β V reduction as in (c).

2. Let R, x 1 : A 1 , . . . , x n : A n N : (α, e), σ be a variable substitution with dom(σ) ⊆ {x 1 , . . . , x n } and assume

N [σ] → M . Then N [σ] ↓ ∈ SC R (α, e). 3. M [V] ↓ ∈ SC 4. M [V] ↑ ∈ SC 5. If M → M , then M ∈ SC 6. V{σ} ⊆ SC
Proof. 1. The V i are inert, and if one does not perform a reduction involving M by either reducing inside, propagating reference substitutions or performing a β V reduction, then the only possible reduction are the propagation of V, which terminates.

Consider an infinite reduction of Λ(N [σ]

). By the previous point, the subterm M must be reduced in at some point. Since the variable substitution forbids any other reduction than propagating itself first, M is the only possible reduct. Then, then term we obtain after reducing N [σ] to M in head position is bounded by a reduct of Λ(M ) which is (SN) by hypothesis on M M. Thus Λ(M ) has no infinite reduction sequence and Λ(M ) is (SN).

Similarly, consider (for suitable (V i )) a (M , (V i )) reduction. If N [σ] is never reduced, then no upward substitution is ever produced. If N [σ] is reduced at some point, it is reduced to M and thus produces a finite amount of SC upward substitutions from here since M is (WB). Hence N [σ] is (WB).

3. We have the following relation: Λ(M [V] ↓ , U, (N i )) Λ(M, (U, V), (N i )) (for appropriate U, (N i )). As the latter is (SN) since M is SC, so is the former. For (WB), we can easily map a (M , (W i )) reduction to a (M, (W i )) by just appending V to (W i ) and start with a → i reduction. Since M ∈ SC, M is (WB).

4. Let M = M [V] ↑ . We proceed by induction on the length of the type α.

For base type, it is clear that M is (WB) if and only if M is (it either produces the same upward substitutions as M , or V) and M [U] ↓ has exactly the same reductions as M [U] ↓ excepted for commutations of upward and downward substitutions, and a possible (subst ). Since M is (SN), so is M .

Now, for α = A e 1
→ α , consider an infinite reduction of Λ(M , U, (V i )). If the upward substitution is never moved upward, we can map this to an infinite reduction of Λ(M, U, (N i )) for the same reasons as above, but the latter is (SN). Thus at some point the upward substitution must go up, so that the head term becomes

M (V 1 [V] ↓ )[W] λ [V] ↑ where W is either V, U or V, M is either a reduct of M [U] ↓ or a reduct of M , and V 1 is either V or V 1 [U] ↓ . By hypothesis, M ∈ SC R (A e 1 → α , e), thus P = M V 1 ∈ SC R (α , e ∪ e 1
). By induction hypothesis, P [V] ↑ ∈ SC R (α , e ∪ e 1 ). We can then bound the considered reduct of Λ by a reduct of Λ(P [V] ↑ , (U, V), (V 2 , . . . , V n )) which is strongly normalizing. 5. This is straightforward from the definition of SC sets.

6. Combining 2. and 4., as for r ∈ dom(U ), V ∈ U(r), V {σ} is the immediate reduct of U [σ] using a (subst) rules.

We can finally give a complete proof of soundness:

Proof. Proposition 4.3.9 Assume that R; x 1 : A 1 , . . . , x n : A n M : (α, e). We have to prove that for any substitution σ with dom(σ) = {x 1 , . . . , x n } and (∀i :

1 ≤ i ≤ n), σ(x i ) ∈ SC R (A i , ∅), then M [σ] ∈ SC R (α, e).
We perform the proof by induction on the structure of M , and use the characterization of Lemma 4.3.12 to prove that terms are strongly computable. ) is strongly computable. By 1. of Lemma 4.3.17, for a reduction of a corresponding Λ to be infinite, a β V reduction between λx.M [σ] and V 1 must occur. The head term has then the form • M = get(r) : get(r)[σ] → get(r). By 2. of Lemma 4.3.17, it suffices to show that get(r) ∈ SC R (α, e). Consider an infinite reduction of Λ(get(r)). By 1. of Lemma 4.3.17, the get(r) must be reduced at some point and from this point it is either replaced by

• M = x : x[σ] reduces to σ(x) ∈ SC R (A i , ∅) ⊆ SC R (A i ,
M [σ][x → V ][W] ↓ with W being either ⊥ or V. M [σ][x → V ] → M [σ, x → V ] which is in SC R (B,
V ∈ V(r) ∈ SC R (R(r i ) = α, ∅) ⊆ SC R (α, e)
and from this point the reduct is bounded by a reduct of a strongly normalizing Λ(V, V, (V ii )), or it just get rid of the downward substitution V and from this point the only possible reductions left are propagation of the initial V which must terminates.

• M = M [τ ], then M [σ] → M [τ, σ]. M
• M = M [U] ↓ : M [σ] → M [σ][U{σ}] ↓ . By induction, M [σ] ∈ SC R (α, e)
and by 6. of Lemma 4.3.17 , r ∈ dom(V) =⇒ V ∈ U{σ}(r) ∈ SC R (R(r i ), ∅). We conclude by parts 3. and 2. of Lemma 4.3.17.

• M = M [V] ↑ : We proceed in the same way, by parts 2., 3., and 4. of Lemma 4.3.17.

• M = M 1 M 2 [V] λ : M [σ] → M = (M 1 [σ]) (M 2 [σ])[V{σ}] λ . By inversion of typing rules, R; Γ M 1 : (A e 1 → α, f 1 ) and R; Γ M 2 : (A, f 2 ) with f 1 ∪ e 1 ∪ f 2 ⊆ e.
By induction and 6. of Lemma 4.3.17,

M 1 [σ] ∈ SC R (A e 1 → α, f 1 ) ⊆ SC R (A e 1 → α, e), M 2 [σ] ∈ SC R (A, f 2 ) ⊆ SC R (A, e), and r ∈ dom(V) =⇒ V{σ} ⊆ SC R (R(r), ∅).
Assume the existence of an infinite reduction of sequence Λ(M , U, (V i )) for appropriate U and (V i ). Assume that no β V reduction between a reduct of M 1 [σ] and M 2 [σ] happens. That is, the reducts of Λ(M ) are of the form

M k 1 M k 2 [W k ] λ V 1 . . . V n .
Notes that the M k i are not exactly reducts of M i [σ]: indeed, the two subterms may freely exchange reference substitutions. This is where the (WB) comes into play: if we abstract the context of the

M k 1 s, that is [.] M k [W k ] λ V 1 . . . V n ,
which can drop some downward substitutions coming from the reduction of M k 2 at any time, this precisely corresponds to an environment reduction. That is, the sequence M 1 [σ], M 1 1 , . . . , M k 1 , . . . is precisely an environment reduction for some sequence of substitution X k 1 . This is also the case form the point of view of M 2 [σ]. As the downward reference substitutions dropped on M k i corresponds either to U or to a substitution previously generated by M k 1-i , they are all strongly computable. Thus the environment reduction satisfies the required hypothesis to apply (WB), and we deduce that only a finite number of substitutions is exchanged between the M k 1 s and the M k 2 s. After k ≥ n steps of reduction for some n, the M k 1 s reduces in isolation. If we take the trace of all the substitutions it received from the environment before this point, and merge them into one big substitution X 1 , then we can see that Lemma 4.3.8). Thus at some point, M k 1 can not reduce anymore. We can do the same for M 2 [σ], and we see that for the reduction of Λ to be infinite, a β v reduction must eventually happens between a M k 1 and M k 2 . Hence there is a k 0 such that M k 0 1 = (λx.P ) and M k 0 2 = U , and the reduct of Λ is of the form (λx.P ) U [Y] λ V 1 . . . V n where Y is composed of substitutions of X 1 , X 2 and U, which are all strongly computable. The β V reduction leads to the term (P

M n 1 is bounded by a reduct of M 1 [σ][X 1 ] ↓ . Since M 1 [σ] is strongly computable, in particular M 1 [σ][X 1 ] ↓ is strongly normalizing (cf
[x → U ][Y] ↓ ) V 1 . . . V n . This term is bounded by a reduct of M 1 [σ] U V 1 . . . V n [X 1 , X ∈ , U] ↓ . But the latter term is strongly normalizing, because M 1 [σ] ∈ SC R (A e 1
→ α, e) and U ∈ SC R (A, e) by 3. and 4. of Lemma 4.3.17. Hence Λ has no infinite sequence reduction, and is (SN).

We apply a similar reasoning to prove that it is (WB).

• M = M 1 M 2 : this is handled as in the previous case (this case is simpler as there is not β V reduction involved).

λ C and λ cES

In this section, we study the relation between λ C and λ cES . Although they are close one to another, λ C is not a proper sub-language of λ cES because of the disappearance of stores and of the set(r, V ) construct in λ cES . We can however give a straightforward translation of λ C in λ cES (Definition 4.4.2). We prove a simulation theorem for this translation, with respect to the non-deterministic version of the reduction of λ cES (cf Definition 4.1.9). Since λ cES features explicit non-deterministic sums and a confluent reduction on sums, while λ C has a non-deterministic reduction defined on simple terms, switching to the nondeterministic version of the reduction of λ cES seems to be the natural way to relate the two languages through a simulation.

A simulation between non-deterministic languages is however weaker, in some sense, than in a setting where both languages are confluent. To explain why, take two ARS (X, → a ) and (X, → b ) with the same set of terms (to simplify, we take a special case of a translation where both languages are the same and the translation is the identity). We also assume that the normal forms in the two ARS are the same, and that they are integers, representing the result of a computation. Assume there is a simulation between the two: if x → * a x , then x → * b x . In particular, this simulation ensures that if x reduces by → a to a normal form, x → * a n ∈ N, then x reduces by → b to the same normal form: x → * b n. If both ARS are confluent, by unicity of normal forms, this is in particular the only possible normal form that x can reach by → b reductions: if x → * b n ∈ N, this implies n = n . On the other hand, if (X, → b ) is not confluent, then nothing prevents x to reduces to many other integers in addition to n. The simulation is then not completely satisfying anymore, as it does not strongly support the claim that the two systems are behaving in the same way. If one chose a meaningless but permissive reduction (for example → b = X 2 \ {(n, t) | (n, t) ∈ N × X}) then the ARS (X, → b ) vacuously simulates (X, → a ) for any choice of → a . Simulation states that → b can do as much as → a , but it does not prevent it from doing much more.

To strengthen the claim that the two languages do behave similarly, we show an adequacy theorem for typed terms, which role is precisely to show that λ cES can not do much more than λ C . If one looks at the possible results of a computation and discards pathological terms to only keep (parallel of) values, these values are essentially the same in for a term of λ C and its translation in λ cES .

We start with a presentation of λ C based on [START_REF] Madet | Complexité Implicite de Lambda-Calculs Concurrents[END_REF].

The concurrent λ-calculus λ C

λ C is a call-by-value λ-calculus extended with:

• a notion of threads and an operator for parallel composition of threads,

• two terms set(r, V ) and get(r), to respectively assign a value to and read from a reference,

• special threads r ⇐ V , called stores, accounting for assignments.

When set(r, V ) is reduced, it turns to the unit value * and produces a store r ⇐ V making the value available to all the other threads. A corresponding construct get(r) is reduced by choosing non deterministically a value among all the available stores. For example, assuming some support for basic arithmetics consider the program (λx.x + 1) get(r) set(r, 0) set(r, 1). It consists of 3 threads: two concurrent assignments set(r, 0) and set(r, 1), and an application (λx.x + 1) get(r). This programs admits two normal forms depending on which assignment "wins": the term 1 * * r ⇐ 0 r ⇐ 1 and the term 2 * * r ⇐ 0 r ⇐ 1. In this language, the stores are global and cumulative: their scope is the whole program, and each assignment adds a new binding that does not erase the previous ones. Reading from a store is a non deterministic process that chooses a value among the available ones. References are able to handle an unlimited number of values and are understood as a typed abstraction of possibly several concrete memory cells. This feature allows λ C to simulate various other calculi with references such as variants with dynamic references or communication [START_REF] Madet | Complexité Implicite de Lambda-Calculs Concurrents[END_REF]. The language is endowed with an appropriate type and effects system ensuring termination.

Reduction

As in λ cES , the operator is subject to structural rules, namely associativity and commutativity, given in Table 4.4. Once again, contexts are similar to the ones of λ cES : we can reduce in any thread at top-level, and the reduction is an usual call-by-value one, excepted that we chose a version which is neither left-to-right nor right-to-left Table 4.5. Reductions rule are given in Table 4.6. There are three of them:

• β v is a call-by-value β-reduction rule • (get) replaces a get(r) occurrence by V , where r ⇐ V is an available assignment at top-level

• (set) generates a new assignment r ⇐ V at top-level Notation 4.4.1. For terms M, V of λ C , we denote by M {x/V } the usual implicit substitution:

• x{x/V } = V • y{x/V } = y when y = x • λy.M {x/V } = λy.(M {x/V }) • (M N ){x/V } = (M {x/V }) (N {x/V })
• get(r){x/V } = get(r)

• set(r, U ){x/V } = set(r, U {x/V })

P P = P P (P P ) P = P (P P )

(β v ) C[E[(λx.M ) V ] → C[E[M {x/V }]] (get) C[E[get(r)]] r ⇐ V → C[E[V ]] r ⇐ V (set) C[E[set(r, V )]] → C[E[ * ]] r ⇐ V

Typing rules

The stratification conditions and subtyping rules are exactly the same as for λ cES . We only give the typing rules of terms in Figure 4.4.

Simulation

We start by defining a translation of a term of λ C in λ cES . set(r, V ), which is not a construct of λ cES , is translated to * [V] ↑ where V = {r → [V ]}. Stores should be converted to reference substitutions. However, they may be placed at many intermediate locations in the structure of a term. We chose a canonical representation, where the downward reference substitutions corresponding to stores are pushed down to the maximum. Then, as reference substitutions vanishes on values, the only remaining ones are the λ-substitutions at application, and the one that are followed by a get(r). The absorption lemma (Lemma 4.4.9) (resp. diffusion lemma (Lemma 4.4.10)) studies how the translation of a term interacts with new downward reference substitutions (resp. upward reference substitutions). Lemma 4.4.9. Absorption Let M be a term and S = S r ⇐ V be a store of λ C , C and E be context of λ cES , and

V = {r → [V ]}. Then C[E[M S [V] ↓ ]] → * nd C[E[M S ]]
Proof. Lemma 4.4.9 By induction on M , using the definition of S and the (subst-r) reductions. Let M be a term of λ cES . Then

E S [M [V] ↑ ] → * nd E S [M ][V] ↑ (4.1) M [V] ↑ N S → * nd (M N S )[V] ↑ (4.2) E S [M [V] ↑ ] N S → * nd E S [M ] N S [V] ↑ (4.3)
using only rules (subst-r) or (subst-r').

Proof. Lemma 4.4.10

• For (Equation (4.1)), we work by induction on E. As we will need Lemma 4.4.6, we add the induction hypothesis that the rule (subst-r' ) is not used.

-E S = [.] nothing to do

-E S = E S M S [U] λ By IH, E S [M [V] ↑ ] → * nd E S [M ][V]
↑ using no (subst-r' ) rules. We use Lemma 4.4.6 and get

E S [M [V] ↑ ] → * nd (E S [M ][V] ↑ ) M S [U] λ
We then apply (subst-r' lapp ) to get

E S [M [V] ↑ ] → * nd (E S [M ]) (M S [V] ↓ )[W] λ [V] ↑
Using Lemma 4.4.9, we get that the right part of the application reduces to M S . Finally, by definition of S , the right hand side is

E S [M ][V] ↑ .
-Other cases are treated alike

• To prove (Equation (4.2)), we apply (subst-r' ). We then use Lemma 4. • Finally, we prove (Equation (4.3)) by combining the two results. We first use the strengthened version of (Equation (4.1)), so we can apply Lemma 4.4.6 and get To prove the induction step, consider a reduct M of M . We use Lemma 4.4.17 to get M → * M P for some reduct P of P , such that the reduction to M doesn't use (subst-r get ). Thus, by Lemma 4.4.16, NF(M ) = NF(M ). By induction on M , ∀T ∈ NF(M ), ∃Q, P → * Q and T Q. But this is true for any reduct M , and we have NF(M ) = M →M NF(M ), hence this is true for M .

E S [M [V] ↑ ] N S → * nd M [V] ↑ E S [M ] N S We

Summary

In this chapter, we presented a lambda-calculus with concurrence and references, featuring explicit substitutions for both variables and references. We discussed the issues explicit substitutions raise with respect to termination and explained how standard techniques fail to address them.

The main contribution of the chapter is a solution to this problem. Reminiscent of Game Semantics, the proof technique we apply is interesting in its own right. Based on an interactive point of view, it is reasonable to expect that the general methodology we present can be extended to other settings, such as proof nets or concurrent calculi.

This work we open the way to the encoding of a calculus with references into differential proof nets, which is done is Chapter 5.

Discussion

Comparison with Other Languages One may wonder how λ cES compares to other concurrent calculi and especially the language λ C presented in Section 4.4.1. In particular, λ cES is almost an explicit substitution version of λ C . Indeed, it turns out that we can define a translation of λ C to λ cES . The weak reduction of λ cES prevents variable substitutions from percolating under abstractions, and translated terms may evaluate to closures as λx.(M [σ]) instead of the expected λx.(M {x 1 /σ(x 1 ), . . . , x n /σ(x n )}) if dom(σ) = {x 1 , . . . , x n }. Up to this difference there is a simulation of λ C in λ cES (Theorem 4.4.5).

More generally, we followed the design choice of adopting cumulative stores, while many languages in the literature and in practice follow an erase-on-write semantics. Remarkably, our choice makes the version with explicit substitutions asynchronous, as various upward and downward substitutions may be reduced arbitrarily without the need of any scheduling. Another point that justifies its introduction is that such calculi simulate a lot of other paradigms, such as erase-on-write or communication channels for example, as mentioned in [START_REF] Madet | Complexité Implicite de Lambda-Calculs Concurrents[END_REF]. This means that the termination of the cumulative store version implies the termination of the aforementioned variants. To illustrate our point, let us quickly sketch how a calculus with explicit substitutions with an erase-on-write semantics could be devised. First, encode set(r, V ) as ((λx. * [r → [V ]] ↑ ) * ). Then, when an upward substitution becomes reducible, apply all possible downward and upward structural rules until it is not possible anymore. Finally, instead of merging reference substitutions, the upper one erases the lower one. Its termination follows immediately from the one of λ cES .

Explicit substitutions and Linear Logic Proof nets are strongly connected to systems with explicit substitutions (see e.g. [START_REF] Accattoli | Proof nets and the call-by-value λ-calculus[END_REF]). λ cES anticipates the translation presented in Chapter 5: its constructs are already inspired by the approach of [START_REF] Ehrhard | Interpreting a finitary pi-calculus in differential interaction nets[END_REF] and [START_REF] Tranquilli | Translating types and effects with state monads and linear logic[END_REF]. λ cES can be seen as a calculus-side version of the nets we will be translating to. The translation and simulation of λ C in λ cES could be described as a compilation from a global shared memory model to a local message passing one. The correctness of this compilation requires that a well-typed strongly normalizing term in the initial language is also strongly normalizing in the target language, and this is what this chapter achieves.

Chapter 5 Encoding a concurrent λ-calculus in nets

In this chapter, we put the devices developed in Chapter 3 to use by presenting a translation of λ cES -the language introduced in Chapter 4 -in the nets described in Chapter 2. The translation builds on ideas from [START_REF] Tranquilli | Translating types and effects with state monads and linear logic[END_REF] for the encoding of references, and from [START_REF] Ehrhard | Interpreting a finitary pi-calculus in differential interaction nets[END_REF] for concurrency, which inspired the routing areas.

We build on the standard call-by-value translation of the λ-calculus in proof nets [START_REF] Maraist | Call-byname, call-by-value, call-by-need, and the linear lambda calculus[END_REF]. In this translation, terms are interpreted as nets, where the interface of the resulting net corresponds to its output (the result of the whole term) as well as free variables. This embodies the different ways a term can interact with an environment, such as a when it is put inside a context. Free variables, that may be substituted by values, are the inputs. The eventual result that the term returns is the output.

In λ cES , references add new possibilities of interaction. Each reference r on which a well-typed term may act, appearing in the effect e of its typing judgement, adds a new input and output capability. The input corresponds to reads from the reference r through a get(r), that can substituted by a downward reference substitutions. The output corresponds to assignments, implemented by the upward reference substitutions generated by the term. Thus for each such reference, the translation of a term M of λ cES will have a new pair of input/output free wires in addition to the wires of free variables and the output. These are the wires that are combined using routing areas. After the presentation of the translation, we give a simulation, a termination and an adequacy theorem.

In order to translate well-typed terms of λ cES in nets, we must also translate types and effects: this is where the monadic translation of [START_REF] Tranquilli | Translating types and effects with state monads and linear logic[END_REF] comes into play. It gives a technique to encode stratified type and effects to formulas of multiplicative linear logic. This allows us to label the input and output wire of a reference r by a standard LL formula.

Overview In Section 5.1, we explain the translation in detail. We start by translating type and effects in Section 5.1.1. We explain how effects are combined using routing areas in Section 5.1.2. Then, Section 5.1.3 explain how terms of λ cES are translated to nets.

The following sections are dedicated to the study of the properties of the translation. In Section 5.2, we state and prove a simulation theorem .

In Section 5.3 shows a termination and adequacy theorem. In Section 5.3.1, we prove that the translation of a term is weakly normalizing. In Section 5.3.3, we prove that the values we obtain by normalizing a term and the ones obtained by normalizing its translation are essentially the same.

After discussing the chapter in Section 5.5, Section 5.6 finally concludes with perspective of future work.

The Translation

Translating types and effects

Before translating terms, we need to translate the types from the type and effects system of λ cES to plain LL formulas. We use the approach of [START_REF] Tranquilli | Translating types and effects with state monads and linear logic[END_REF], a monadic translation, explained in the following. Before translating to LL, let us first try to take a type with effects and translate it to a pure simple type. Let e = {r 1 , . . . , r n } be an effect (a finite set of references), assume we can assign a simple type R i to each reference r i . The type a store representing the current state of the memory would be S e = R 1 × . . . × R n . We transform a term M of type A producing effects to a pure term which takes the initial state of the store, and returns the value it computes together with the new state of the store after this computation. Using curryfication for the arrow type, we define the following translation:

T e (α) = S → S × α T e (A e → α) = A → (S → (S × α)) ∼ = A × S → S × α
From there, we go to LL types by implementing the pair type A × B as !A ⊗ !B, and the usual call-by-value translation for the arrow (A → B) • = !(A • B • ) [START_REF] Maraist | Call-byname, call-by-value, call-by-need, and the linear lambda calculus[END_REF]. We still have to determine each R i first. Using the previous formula, we may associate an LL type variable X r i to each reference and plug everything in to obtain the following equations (where A i is the type given to r i by the reference context):

Unit • = !1 (A {s 1 ,...,s m } → α) • = !((A • ⊗ X s 1 . . . ⊗ X s m ) (X s 1 ⊗ . . . ⊗ X s m ⊗ α • )) X r i = A i •
This system is solvable precisely because the type system is stratified [START_REF] Tranquilli | Translating types and effects with state monads and linear logic[END_REF], and we can thus translates all the types of λ C to plain LL types. The behavior type B will be translated to types of the form A 1 `. . . `An , as the translation indeed remembers the types of each threads.

Combining effects

The monadic translation allows to translate a type and effect to a plain LL type. Each reference appearing in the effects e of the type of a term will have two corresponding wires in the translation, one for the input and the other for the output. When the effects of two subterms must be combined, mainly in the application case and the parallel case, these wires are connected through routing areas. More precisely, we use two specific routing areas which we introduce below: the γ area and the δ area. In the following, E i = {1, . . . , i} and R i is the binary relation defined on

E i by k R i l ⇐⇒ k = l.
The γ area is defined by (E 3 , E 3 , R γ = R 3 ). It is composed of 3 pairs of input and outputs grouped by label. Each such pair represents a plug to which translated terms will be connected. The definition of R γ expresses that the input and the output of a plug are not connected, as a component should not receive the data it sent himself: this would be the analog of a short-circuit. All others inputs and output are connected.

The δ area is an analog structure with 4 plugs: (E 4 , E 4 , R δ ). It is designed to handle the application M N which includes three potential sources of effects :

1. The effects e 1 produced by reducing M to λx.M

2.

The effects e 2 produced by reducing N to value V N

3.

The effects e 3 produced by reducing M [V N /x] to the final result V

The reduction of λ C imposes that e 1 and e 2 happen before e 3 , while e 1 and e 2 may happen concurrently. For 1 ≤ i ≤ 3, the plug (i, i) of δ corresponds to the effects e i . The last one is the external interface for future connections. We easily accommodate δ to implements the sequentiality constraint by removing the couples (3, 1) and (3, 2) from R 4 to form R δ . Indeed e 1 and e 2 happens before e 3 thus cannot observe any assignment made by the latter.

To implement it, we just cut the corresponding wires. We see that the formalism of routing areas allows us to easily encode the order of effects.

We are now ready to give the translation of terms.

Translating terms

The general form of the translation of a term x 1 : A 1 , . . . , x n : A n M : (α, {r 1 , . . . , r k }) is given by M

• α • !X r k r k !X r k r 1 !X r k r k !X r 1 r 1 A • 1 x 1 A • n x n
We distinguish three different types of free wires:

Output wire The right wire, labelled by α • , corresponds to the result of the whole term.

Variable wires Each wire on the left corresponds to a variable of the context. The explicit substitution of a variable x for a term V • is obtained by connecting the output wire of V • to the wire of x.

References wires

The wires positioned at the top are input wires corresponding to references and have a similar role as variable wires, while the wires at the bottom corresponds dually to the output. References wires will be connected by routing areas.

We give the different cases of the translation above. get(r) and reference substitutions demonstrate how reference wires interact with the rest. The abstraction shows how effects are thunked in a function's body following the monadic translation. Application and parallel use the routing areas to handle effects scheduling. Variable substitutions are handled in a traditional way, using a cut (or, in nets, just a connection).

In all constructions, the different variable wires corresponding to multiple occurrences in subterms of a variable appearing in the context are unified through a contraction. The var rule is encoded as an axiom, while the constant * is encoded as a !1. The axiom is eta expanded, hence it is surrounded by an exponential box. The wires corresponding to variables that are not free in the term but appear in the context are provided by weakenings. Note that the weakenings are willingly put inside the exponential boxes: thanks to the closed box constraint of the reduction, this reflects the sequentiality of the term as it requires that all free variables are effectively substituted before a variable or a * may be itself moved around. This is required for both adequacy and termination.

Variable substitution (Figure 5.1) A variable explicit substitution is naturally built by connecting the output wire of a substituted value to the corresponding variable wire.

Get and reference substitutions (Figures 5.3 to 5.5) An upward reference substitutions M [V] ↑ packs the output of the translation of V with the output reference wire corresponding to r of M using a cocontraction. One important remark is that in the translation of a reference substitution V, an additional exponential layer is added around the translation of V . In a call-by-value language, the non determinism is strict in the sense that nondeterministic terms must be evaluated before any copy. For example, the term (λx.f • The first one allows to discriminate what nets can be the target of structural rules, which implements substitution. In call-by-value, the only terms that can be substituted are values. The ! is introduced by the translations of values, using ! p , and eliminated at usage -when applied to another termfor each copy by a dereliction.

x x) get(r)[r → [V 1 , V 2 ]] ↓ can reduce either to f V 1 V 1 or f V 2 V 2 but not to f V 1 V 2 . Differential LL rather implements call-by-name semantics of the R Γ R; Γ get(r) : (A, {r}) (get)
• The second usage relates to the differential part. The bang denotes resources that may be packed non deterministically by a cocontraction. The choice is made when a dereliction is met.

But as we noted, these two usages are in contradiction: a non-deterministic packing should not be allowed to be substituted. Technically, the dereliction corresponding to the place of usage and the dereliction corresponding to the nondeterministic choice should not be the same. This is the reason of the additional ! layer introduced by an exponential box around V • . The corresponding dereliction is found in the translation of get(r). The get(r), dual of the set, takes a resource from the corresponding input reference wire and redirects it to the output wire. It outputs a coweakening on the reference wire as it does not produce any assignment. As mentioned in the previous case, a dereliction is added on the input wire to force the non-deterministic choice and strip the exponential layer added by the set. Application and parallel (Figure 5.7) The application puts the routing area at use. Using the same terminology as in the introduction of this section, we see the effects e 1 and e 2 coming respectively from the evaluation of M and N , and e 3 , liberated by the body of the function being applied, plugged accordingly on the δ area. The parallel operator is similar to the application, but simpler. The two outputs of the terms are connected using a `. Unlike application, there is no constraint on the order of effects, thus reference wires are connected through a symmetric γ area. Note that the translation of a value V is an exponential box. This box is We now study the properties of this the translation, starting with simulation.

i = 1, 2 R; Γ P i : α i R; Γ P 1 P 2 : B (

Simulation

The simulation theorem states that a reduction step in the source language is reproduced by zero or more reduction in nets. To derive this result, we define a notion of typed context and a translation of contexts to nets.

Nets contexts

Reduction rules of λ cES are defined up to contexts (see Table 4.3). To prove simulation, it is natural and convenient to give contexts a proper treatment, by providing a notion of typed context and a translation of these contexts to nets. In both cases, this boils down to add a special treatment for the hole, and use the material already developed for terms otherwise. We first extend typing to context: the only additional rule we need is the one for the hole [.]. The other constructors of contexts are the same as the constructors of standard terms, hence we can the same typing rules of terms.

[.] can be seen as a special kind of variable in the typing derivation. But unlike variables, it can be substituted by something else than a value. Using the standard typing rules of λ cES , we can build type derivations of contexts. A context can then be translated to a net, with an interface determined by α and e, labelling free ports. This is what we call net contexts. The substitution of a net in a net context consists in plugging the translation of a term with a compatible type in this interface.

We just extend the translation with a case for the hole. We can then carry on and use the usual term translation to build the translation of a context (C[E]) • , which is a net of the form

The substitution of M • , or of any net with a compatible interface for that matter, in (C[E]) • is defined by just connecting the free wires of the substituted net to the corresponding free wires of the context hole :

The fundamental property of net contexts and net substitutions is that the substitution commutes with the translation, in the following sense :

(C[E[M ]]) • = (C[E]) • [M • ]
The very definition of net reduction immediately entails that if M

• ⇒ * N • then (C[E]) • [M • ] ⇒ * (C[E]) • [N • ].
Together with Proposition 5.2.4, this ensures that we can focus on the case where C = E = [.], as the general case follows seamlessly.

From here, we check that each reduction rule of λ cES can be simulated on the net side, relying on the definition of the reduction and the behavior of routing areas. We will prove the following one-step simulation lemma: Lemma 5.2.5. One-step simulation Let M : (α, e) be a closed well-typed term of λ

cES . If M → N , then M • ⇒ * N • .
To do so, we proceed by case analysis on the reduction rule applied in the reduction M → N .

Variable substitutions reductions

Let us show the case of a (subst) rule. Thanks to the previous theorem, we can assume that contexts are empty without loss of generality. We consider only closed terms. Indeed, since reduction contexts S, C, E do not bind variables, all the terms appearing in the premise of a rule are thus closed terms, and we can omit their context. For each rule, we write the translation of the premise followed by its reduction in nets, which matches the conclusion.

The fundamental rule that performs the substitution is (susbt var ).

(subst var ) (σ(x) undefined) → * (subst var ) (σ(x) defined) → *

When reaching a get(r) or a * , the substitution simply vanishes.

(subst unit ) → *

The (subst app ), (subst subst-r ) and (subst subst-r' ) perform a duplication and propagate the substitution inside reference substitutions. The (subst ) just duplicate the variable substitution to the two threads (subst ) ⇒ *

Finally, the (subst merge ) distributes the outer substitution to both the term and the inner substitution.

(subst merge ) ⇒ *

Downward reference substitutions reductions

The propagation of references substitutions relies on the behavior of routing area, and especially Proposition 3.2.7. The fundamental case is the non deterministic reduction happening when reducing a get(r) whose redex is (subst-r get )

Then for each V in the image of V, there will be exactly one summand of the following form

⇒ *
The remaining term reduces to the translation of get(r): ⇒ * (subst-r val ), (subst-r ) and (subst-r app ) are just direct application of the Proposition 3. (subst-r merge ) and (subst-r subst-r' ) amount to nothing in nets, as the translation already identifies the redex and the reduct of these rules.

(subst-r subst-r' ) (subst-r merge )

Upward reference substitutions reduction

As for downward substitutions, the main ingredient is the Transit lemma, applied to our specific routing area δ and γ.

(subst-r' ) ⇒ *

(subst-r' lapp )

⇒ *

(subst-r' rapp ) ⇒ *

Termination and Adequacy

Termination

In this section we show that the nets that are the translation of a well-typed terms of λ cES are weakly normalizing. Nets are indeed more liberal in their reduction: for example, they reduce an expression corresponding to a β-redex (λx.M ) N even if N is not a value (take a get(r)) for example. There also administrative reductions, corresponding to merging of routing areas, which are invisible on the calculus side. As a result, the translation of a normal form of λ cES my not be a normal net. The goal of this section is to show that however, the translation of a normal form of λ cES can be reduced in a few steps to a normal net that can be related to the original term.

Proof of Proposition 5.3.1

To prove Proposition 5.3.1, we proceed in two stages: first, we extend λ cES to a language λ cES + that is able to perform more reductions than λ cES , precisely the kind of generalized β reduction mentioned above. The extension of the translation and the simulation theorem for λ cES + are straightforward. Then, we show that λ cES + also terminates, give an explicit grammar for its normal forms, and show that the translation of these normal forms are strongly normalizing nets.

Working on the calculus

We add a labelled reference substitution variable substitution to λ cES :

M [|V|] ↓ | M [|x/N |].
The first one, M [|V|] ↓ , corresponds to a downward reference substitution where V has no free variables. The second one corresponds to a variable substitution of a term that is not a value. Both can appear during the reduction in nets but are not accounted for in λ cES . M [|x/N |] cannot be reduced, either in N or by (subst) rules (whether N is a value or not). The labelled variable substitution forbids any reduction under it, except for the labelled reference substitutions. We extend the reduction rules (subst-r) to the labelled substitution [|V|] ↓ . They can be performed anywhere (included under a variable substitution) except under abstraction, as defined by the following reduction contexts:

J ::= [.] | J M | M J | J[V] ↓ | J[σ] | J[|x/N |].
We add a generalized β-rule which fires such labelled substitution :

(β ) (λx.M ) N [V] λ → M [|V|] ↓ [|x/N |]
This corresponds to the additional reduction nets can do. A β redex can always be fired in nets even if the argument is not a value. But then, the corresponding term do need to be reduced before any duplication, erasure or substitution. Let us now show termination and describe the normal forms of λ cES +: Definition 5.3.1. F -normal forms Let M be a normal form of the form of λ cES . It belongs to the grammar M norm (cf Lemma 4.2.7). Then M reduces to a sum of terms in λ cES +, where each summand belongs to the following grammar of F -normal forms :

F norm ::= get(r) | F norm V [V] λ | F norm F norm [V] λ | M [|x/F norm |]
where the M is in λ cES (contains no labelled substitution).

Proof. By induction on the structure of M , with the additional hypothesis that only the additional rules are performed (no upward substitution) :

• M = get(r) : ok Proof. By induction :

• M = M norm V [V]
• M = get(r) : ok ] λ : by induction, F norm is normal, and values are not F -normal form, so the application cannot create any β-redex.

• M = F norm V [V
• M = M norm M norm [V] λ : same as the previous case

• M = M [|x/F normal |] : the explicit substitution prevents any reduction except (subst-r) ones for labelled reference substitution, but by definition, M does not contain any.

Values As stated above, we can first observe that the translation of * , of a variable x and an abstraction all satisfy the separability conditions. Indeed, they are composed of a box with at least one auxiliary door, and the inside of the box is a normal form (by induction for abstraction and trivially for others). As they are pure terms, m = n = 0.

Get It is almost the same as values, except that the output o corresponding to the reference of get(r) is connected to a dereliction, which is allowed in (b).

Application By induction, M • and N • are separable, thus can be decomposed in the following way :

We can merge the 3 routing areas R, R 1 and δ. All the inputs or outputs previously connected to one of the small areas immediately satisfy the conditions (b,c) by IH. The two remaining wires i and o are respectively connected to the auxiliary port of a par and the auxiliary port of a cocontraction, thus satisfy (b,c). S and S 1 are normal by IH, and the translation of V is easily seen as normal. O is the conclusion of a par, hence satisfies (b,c). It only remains to see that the whole net excepted the routing areas is normal, but the only redex that could appear is the connection of a dereliction to M • . By (c), the output of M • is either the conclusion of an open box or a par which do not form a redex. The condition (a) is verified.

Parallel Similar to application

Variable substitution As for application, we apply the IH on M • and V • , merge the routing areas, and just check that the connection of V • to M • cannot create new redexes using (b) on the output wire of V • .

Reference substitutions Again, the same technique is applied. translation of a term (which exists thanks to weak normalization and is unique by confluence) corresponds to the value in the normal form of the term in λ cES : if we discard terms that deadlocked, the term and its translation computes the same values.

Discussion

Termination We believe that the result of weak normalization for the translation of well-typed terms of λ cES may extend to a strong normalization result. This was the idea behind the (T 1 ) of Section 2.4: it ensures that weak normalization is actually sufficient to get strong normalization. The problem we encountered is that we use the 0 → reduction (or at least on of its avatar n →, mentioned in Remark 3.1.7) in the reduction concerning routing areas such as application of the transit lemma , which potentially breaks the (T 1 ) property (Definition 2.4.3). However we use it in a restricted manner: we use it just to implement the neutrality of coweakening with respect to cocontraction (as does n →). In practice, we always erase a summand that was produced by the previous duplication of an initial term as two summands, by a ba → reduction. This kind of reduction should not break the (T 1 ) property, as any potential looping subnets that is erased is still present in other summands.

Concurrency and correctness

We mentioned from Chapter 2 that the translation of concurrent program may produce nets that do not respect the correctness criterion of differentials LL. A simple example is the following well-typed term of λ C : P = (λx.set(r, x)) get(r) (λx.set(r, x)) get(r)

This term does not reduce further, but it can be modified easily to normalize to a parallel of values: P set(r, * ), for example, reduces to * * r ⇐ * r ⇐ * r ⇐ * . This is a core example of a program that is translated to a net which has a cycle in one of its switching graphs (cf Section 3.1.3 for a review of the correctness criterion). The cycle correspond to a seemingly cyclic dependency in the term P : in the left thread, the x depends to the value get(r) for which it will be substituted. Then, the set(r, x) depends on this x. From the outside, the fact that the set is executed after the get is not visible. Thus, the right thread just see a term that is likely both read from and write to the reference r. Because of this, there is a dependence between the right get(r) and the left set(r, x). As the program is totally symmetric, we can see the emergence of a cycle: from the left get(r), to the left set(r, x), to the right get(r), to the right set(r, x), to the left get(r). This is not an actual cyclic dependency it the languages between some of the junctions are in fact mutually exclusives: the first get(r) being reduced must feed on an external assignment (as the program P alone can not reduce further), breaking the dependency with the adverse set(r, V ). But this kind of dynamic property is hard to accounted in nets. This seems not to be specific to the languages we choose, as this example can be transposed to the π-calculus process P = a(x).a x | a(x).a x and thus already affect the translation presented in [START_REF] Ehrhard | Interpreting a finitary pi-calculus in differential interaction nets[END_REF].

Perspective

Typed and untyped terms The stratification constraint of the type system seems rather restrictive, especially from a practical point of view. It enforces strong normalization, which is a questionable feature for a realistic programming language. Tranquilli [START_REF] Tranquilli | Translating types and effects with state monads and linear logic[END_REF] showed that the stratification constraint precisely corresponds to the solvability of the equation given by the monadic translation, without resorting to recursive types. If one allows recursive types in nets, we can encode non stratified programs, and even untyped programs. The simulation result should also holds in this setting as it mainly relies on the operational semantic of nets, which does not depend on typing nor correctness. On the other hand, it is not obvious that an adequacy result would be achievable, and if it is, how. For this reason, we restricted ourselves to a fragment where these kind of properties may still be established. Concerning termination, a desirable extension of the termination theorem to the untyped case would be the preservation of strong normalization. This property, especially studied in explicit substitutions systems, ensures that the translation of a strongly normalizing term is itself strongly normalizing.

Synchronous and asynchronous effects In the design of the λ cES language, we made some choices in order to get a more asynchronous system. This make the translation in nets easier. The two main such features are the cumulative stores (an assignment do not erase the previous ones, but rather add up), and the fact that the reduction is neither left-to-right nor right-to-left in the reduction of applications. The latter point is not really limiting, as one can encode a specific order of evaluation. Since the reduction is weak (no reduction under abstraction), it suffices to change an application M N to (λx.x N ) M to force a function to be fully evaluated before the argument, and get a left-to-right operational semantics.

The cumulative stores are a more profound design choice. Usual programming languages with imperative references rather implement an erase-on-write semantics: in λ C (cf Section 4.4.1), this would correspond to have exactly one store r ⇐ V for each reference r, and to replace the (set) reduction rule by the following one :

(set') C[E[set(r, V )] r ⇐ U → C[E[ * ]] r ⇐ V
Implementing this kind of behavior in nets requires a form of synchronization. Tranquilli has sketched some ideas about it [START_REF] Tranquilli | References, Multithreading and Differential Nets[END_REF]. He proposes the use of an additional wire for each references that represent a locking signal. get(r) and set(r, V ) must acquire this lock before reading or writing values. While he resorts to second-order constructs (the idea of a transistor already used by Ehrhard and Laurent to encode prefixing in π-calculus [START_REF] Ehrhard | Interpreting a finitary pi-calculus in differential interaction nets[END_REF]) to implement the lock, we could implement it directly in our nets thanks to our reduction operating only on closed boxes. Here is a proposal of a lock mechanism in nets. This lock has two input wires (top) and two output wires (bottom), where the left input and output correspond to the locking signal while the right input and output correspond to the data we want to tie with the locking signal:

The locking signal does not carry any information, but only encode the precedence of memory operations: this is why it is typed by Unit • = !1. The lock multiplexes the locking signal with the data with a tensor, and this pair is then enclosed by an exponential box. This box only serve as a synchronization device, and is directly connected to a dereliction in order to open it, followed by a par which demultiplexes the two inputs. It the reduction were not restricted to closed boxes, then the lock could be instantly reduced to two wires and would just act as the identity on both its inputs, independently of what it is connected to. However, with a reduction restricted to closed boxes, the lock's box must be closed (id est being without auxiliary ports) before being opened. This means that as long as both the inputs are not connected to a closed exponential box, then the lock prevent any interaction between what is connected to its inputs and what is connected to its outputs. When both its inputs are closed exponential boxes, the lock can be removed through the following reduction:

Here is a sketch of how set(r, V ) and get(r) would be encoded using this lock in an erase-on-white setting: The left part corresponds of each encoding to the locking signal, while the right part correspond to the data being effectively exchanged through references. Both encoding start with a dereliction connected to the incoming data, stripping away the additional exponential layer of values stored in references (cf the paragraph on get and reference substitutions in Section 5.1.3). Then, in both case, the lock imposes that the get(r) or the set(r, V ) acquire the locking signal, meaning that they must receive a !1 on the left input, before anything else can happen. For set(r, V ), a second lock prevent V • from being emitted asynchronously, as the first lock have not control on it. When this condition is met, the lock can be removed and the reductions corresponding to copying/sending data may take place. As long as the lock vanishes, the locking signal is consequently re-emitted through the appropriate wire, making it available for the next memory operation to acquire it.

Note that in our current setting of cumulative stores, get(r) and set(r, V ) sends messages asynchronously: a get(r) produces a dummy output through a coweakening, while a set(r, V ) ignore the input through a weakening. Here, a term really takes the current state of the whole store as an argument, and return the new state of the store. In particular, get(r) duplicate the input data, but also re-emits it through the reference output wire. The set(r, V ), by replacing the output with its own data, effectively erases any previous assignment. In this hypothetical system, the additional exponential layer introduced by an exponential box in the translation of reference substitutions is rather introduced here by a codereliction instead, as in the translation of the finitary π-calculus of [START_REF] Ehrhard | Differential interaction nets[END_REF]. The wire corresponding to data would be all connected through communication areas, that is routing areas that allow everyone to communicate with everyone. On the other side, the connection of signals must be done using specific routing areas that precisely implement the ordering of effects, as our δ area, for example. We believe that λ cES would also be adaptable to such a setting, by mimicking the mechanisms we sketched for nets on the calculus side.

Expressivity of the type system Another direction for future work is to enrich the type system of λ cES and λ C . LL can indeed accommodate a lot of possible extensions: second order (polymorphism), sum types (the additive fragment), recursive types (by adding fixpoint operators), etc. One can also add ad-hoc cells and reduction rules in nets to implement additional constants and primitives for the languages, such as integer or floating point arithmetic for example. Depending on the feature, it is not clear yet how it interact with the current setting and if it has a natural representation in nets.

A parallel abstract machine We stressed that we hope to benefit from the ability of nets to enable independent computations to be done in parallel. We think of the GoI abstract machine for PCF introduced in [START_REF] Dal Lago | Parallelism and synchronization in an infinitary context[END_REF] in particular. An extension of GoI for differential nets can be found in [START_REF] De | The Geometry of Interaction of Differential Interaction Nets[END_REF]. Taking inspiration from it, we could adapt the multi-token machine of [START_REF] Dal Lago | Parallelism and synchronization in an infinitary context[END_REF] to work on nets. This would provide an interesting basis for a prototype implementation. Automatic parallelism, sometimes referred as implicit parallelism, is not the only benefit of a such abstract machine. The natural message-passing style of execution makes it very easy to slice a program into arbitrary components and execute them on different computing unit. This is demonstrated for example in [START_REF] Fredriksson | Seamless distributed computing from the geometry of interaction[END_REF], which introduces a PCF-like language enriched with an explicit construct to defer the computation of subterms on different nodes. The corresponding machine is GoI-based one.

Figure 2 . 1 :Figure 2 . 2 :

 2122 Figure 2.1: Example of non-confluence

→

  may be performed. Definition 2.2.1. Reduction → We define the reduction relation → ⊆ S N × P N by: • (Surface) If by an atomic rule, thenNote that R may be empty, which implies that atomic rules are included in →

Definition 2 . 3 . 3 .

 233 Parallel reduction (P N , ⇒ ) is defined as the sum lifting of → . Proposition 2.3.4. Properties of parallel reduction The parallel reduction (P N , ⇒ ) verifies: 1. ⇒ ⊆ ⇒ ⊆ ⇒ *

Figure 2 . 4 :

 24 Figure 2.4: Counter example for (T 1 )

Definition 2 . 4 . 1 .

 241 (P N , ) Let surf → be the union of all atomic reduction rules. Then (P N , ) is the total lifting (P N , ⇒ tot ) of the surface extension of surf → up to context. By surface extension, we mean that we ignore the second point of the definition of the extension up to context and do not allow any reduction inside boxes. Definition 2.4.2. (S N , Then (P N , ) is the total lifting (P N , ⇒ tot ) of the inner extension of inner → up to context. By inner extension, we mean that we ignore the first point of the definition of the extension up to context and only allow reductions inside boxes. Definition 2.4.3. (T 1 ) A rewriting system

Proposition 2 . 4 . 7 .

 247 CommutationLet S * R and R + R . Then there exists S such that Proposition 2.4.7 We proceed by induction on both the length of the reduction S * R and R → + R . We consider first the following diagram where both reductions are one-step : R R

( a )→Figure 2 . 5 :Figure 2 . 6 :

 a2526 Figure 2.5: Cases (a),(b), and (c)

Case 1 :Case 2 :

 12 situation (a),(b) or (c) We perform an induction on the length of the reduction S k R. The induction hypothesis (IH) is that we can fill the diagram in the following way that k ≤ k, and the bottom reduction does not contain any duplication. The base case k = 0 is trivially true. Now, assume S k T R. The upper square of the figure below is obtained by filling the diagram T R R as in Figure 2.5 to get the middle line T * T p . We apply the IH on each step T i T i+1 , which we can do precisely because the IH states that the length k i of the reduction S i k i T i decreases with i. Pasting all the diagrams, we get: situation (d) The case of duplication is simpler as the step R R is reflected by just one step S S in the diagram of Figure 2.6. The IH is that we can fill the following diagram:

Definition 3 .

 3 1.1. Multirelation Let A and B be two sets, a multirelation R between A and B is a map R : A × B → N. Remark 3.1.2

Definition 3 . 1 . 5 .

 315 Composition of multirelationsLet R, S be multirelations respectively between A and B, and B and C, we define the multirelation S • R by

Proposition 3 . 1 →, s 2 →

 312 1.10. Tree reduction Let n ≥ 0, m ≥ 0. We have: Proof. Proposition 3.1.10 By double induction on n and m, usings

  Theorem 3.1.13. [14, Ehrhard-Regnier] Strong normalization of correct nets A correct net is strongly normalizing.

Example 3 . 1 . 19 .

 3119 Let R be the multi relation between L i = {i, i } and L o = {o, o } defined by :

  The corresponding net is obtained by juxtaposing the nets of R and S: R S = R + S

  where S is a routing area defined by (L i -{i}, L o -{o}, S) and S(x, y) = S(x, y) + S(x, o)R(i, y) (3.1) Definition 3.2.4. Trace Let R = (L i , L o , R) be a routing area, and (i, o) ∈ L i × L o such that R(i, o) = 0. We define the trace at (i, o) of R, Tr (i→o) (R), by the routing area obtained by reducing PreTr (i,o) (R) to a normal form.

  Composition Let R = (L i , L o , R) and S = (L i , L o , S) be two routing areas, o ∈ L o and i ∈ L i . The composition of R and S at (i, o) is the routing area R • i→o S = (L i + L i \ {i}, L o + L o \ {o}, T ) defined by R • i→o S = Tr (i→o) (R + S).Remark 3.2.6. This operation can be generalized to the connection of n outputs of R to n inputs of S. When n = |L o | = |L i |, the multirelation T describing the resulting routing area is the composed S • R.

Proposition 3 . 3 . 5 .

 335 Path preservationLet R be a routing net, p 1 and p 2 be free ports, and assume R → R . Then Paths p 1 →p 2 (R) and Paths p 1 →p 2 (R ) are in bijection, which we write Paths p 1 →p 2 (R) Paths p 1 →p 2 (R ).

4

  Let us build the bijection τ :Paths p 1 →p 2 (R) → Paths p 2 →p 2 (R ). Let π ∈ Paths p 1 →p 2 (R) be a path that does not visit the contraction or the cocontraction, it is left unchanged and we set τ (π) = π. Otherwise, we replace any subsequence of π appearing in the left column by the corresponding one in the right column:

Theorem 3 . 3 . 7 .

 337 Routing area characterizationThe normal form of a routing net S is a routing area R = (L i , L o , R).Proof. Theorem 3.3.7 We prove the result by induction on the number n of cells of R.• (n = 0) R is only composed of free ports and wires. We takeL i = {src(w) | w wire }, L o = {tgt(w) | w wire } and R is the relation defined by i R o ⇐⇒ ∃w, i = src(w), o = tgt(w).

Theorem 3 . 3 . 8 .

 338 Path semantic Let S be a routing net. Let L i be the set of free ports of S which are the source of a wire, and L o the ones that are the target. For (i, o) ∈ L i × L o , we write N (i, o) = |Paths i→o (S)| the number of paths between i and o. Then S is the multirelation between L i and L o given by S (i, o) = N (i, o) Proof. Theorem 3.3.8

Remark 4 . 1 . 2 .

 412 The three constructs [V] ↓ , [V] ↑ and [V] λ encapsulate the assignments in terms and in stores presented in the introduction of Chapter 4: there is no need anymore for set(r, V ) and r ⇐ V . See Section 4.6 for a discussion of this aspect.

Notation 4 . 1 . 3 .

 413 Reference substitutions will be sometimes written with the notation

Corollary 4 . 1 . 19 .

 4119 Let M N or M V N .

Proof.

  Proposition 4.1.18 Before simulating the reduction of M in N , we may have to carry around reference substitutions that are at a different level in the two terms. Let us first prove that if M = C[E[P ]], then N → * C[E [P ]], that is we can reduce M to a term with the same prefix C[.] by pushing down pending reference substitutions.

Figure 4 . 1 :

 41 Figure 4.1: Stratification of the type system

Figure 4 . 3 :

 43 Figure 4.3: Typing rules for λ cES

Theorem 4 . 3 .

 43 10. Termination Let R M : (α, e) be a well-typed closed term. Then M is strongly normalizing. Proof. Theorem 4.3.10 Let R M : (α, e). By Proposition 4.3.9, M ∈ SC(α, e). By Lemma 4.3.8, M is strongly normalizing. Since the reduction is locally confluent, we deduce the confluence of the language. Corollary 4.3.11. Confluence The reduction is confluent on typed terms. Proof. Corollary 4.3.11 By Newman's lemma.

Lemma 4 . 3 . 17 .

 4317 Auxiliary results for soundness Let M ∈ SC R (α, e) and V with r ∈ dom(V ) =⇒ V ⊆ SC R (R(r), ∅.

  e 1 ∪ e) by induction hypothesis.

  = x | * | λx.M -terms M ::= V | M M | get(r) | set(r, V ) | M M -stores S ::= r ⇐ V | (S S) -programs P ::= M | S | (P P )

Lemma 4 . 4 .Lemma 4 . 4 . 8 .

 44448 [START_REF] Asperti | Paths in the lambdacalculus. three years of communications without understanding[END_REF] states that the translation is modular with respect to contexts. Lemma 4.4.8 shows that the translation commutes with implicit substitutions. Lemma 4.4.7. Context decomposition Let P be a program of λ C , • If P = C[E[M ]] with C = [.] or C = [.] N , then P = P • If P = C[E[M ]] with C = [.] N S, then P = E S [M S ] N S Proof. Lemma 4.4.7 This is an easy induction following the definition of S . Substitution for S Let M, M be terms, V a value and S a store of λ C . Then M {x/V } S = M S {x/V } Proof. Lemma 4.4.8 By induction

Lemma 4 . 4 .

 44 [START_REF] Danos | The structure of multiplicatives[END_REF]. Diffusion Let N be a term, E a context, S = S r ⇐ V a store of λ C and V : r → [V ].

4 . 9

 49 on N S [V] ↓ to get N S and Lemma 4.4.6 with C = M [.] to get the desired result.

RFigure 5 . 1 :Figure 5 . 2 :

 5152 Figure 5.1: Translation of variable reference substitutions

Figure 5 . 3 :Figure 5 . 4 :Figure 5 . 5 :

 535455 Figure 5.3: Translation of get(r)

Abstraction (Figure 5 . 6 )Figure 5 . 6 : 1 →Figure 5 . 7 :

 5656157 Figure 5.6: Translation of λx.M

Figure 5 . 8 :

 58 Figure 5.8: Translation of parallel

Theorem 5 . 2 . 1 .

 521 Simulation for λ cES Let M : (α, e) be a closed well-typed term of λ cES . If M → * N , then M • ⇒ * N • .

Definition 5 . 2 . 2 .

 522 Hole typing rule R (α, e) R, [.] : (α, e) [.] : (α, e)

Definition 5 . 2 . 3 .

 523 Hole translation We define the translation of a typed hole R [.] : (α, e) as R (α, e) R, [.] : (α, e) [.] : (α, e)

Proposition 5 . 2 . 4 .

 524 Nets substitution Let [.] : (α, e) be a typed hole, [.] : (α, e) C[E] : (β, e ) a typed context, and M : (α, e) a term. Then :

(

  subst app ) ⇒ * (subst subst-r ) ⇒ * (subst subst-r' ) ⇒ *

Proposition 5 . 3 . 1 .

 531 Let N : (α, e) be a closed well-typed term of λ cES which is a normal form. Then N • is strongly normalizing.Together with simulation, this gives the following theorem: Theorem 5.3.2. Weak normalization Let M : (α, e) be a closed well-typed term of λ cES . Then M • is weakly normalizing. Proof. Theorem 5.3.2 Let M : (α, e) be a closed well-typed term of λ cES . By Theorem 4.3.10, it is strongly normalizing, hence M → * N where is normal. By simulation, M • ⇒ * N • . By Proposition 5.3.1, N • is strongly normalizing, and in particular M • ⇒ * N • ⇒ * N where N is a normal form. The next section gives the detailed proof of Proposition 5.3.1.

  λ : by induction, M norm reduces to a sum of F norm . Take one such summand N , then M → * N norm V [V] λ (because no rule (subst-r' ) was used)• M = M norm M norm [V] λ :we proceed as in the previous case• M = V M norm [V] λ : by induction, M norm reduces to some N in F norm grammar, so M → * V N [V] λ .Then, by inversion of typing rules, V is of the form λx.P and we can apply the new β-reduction to get P [|V|] ↓ [|x/N |]. By pushing down [|V|] ↓ in P , we can reduce it to a sum of P i s where each P i do not contain labelled substitutions. Then M → * i P i [x/N ] Lemma 5.3.3. F -normal forms are normal.

Figure 5 . 9 :Figure 5 . 10 :

 59510 Figure 5.9: Encoding of get(r)

  1 A Concurrent λ-calculus with Explicit Substitutions . . . . . . . 4.1.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.1.2 Reduction . . . . . . . . . . . . . . . . . . . . . . . . . . 4.1.3 Weak confluence . . . . . . . . . . . . . . . . . . . . . . 4.1.4 Preorder on terms . . . . . . . . . . . . . . . . . . . . . . 4.2 Stratification and Type System . . . . . . . . . . . . . . . . . . 4.2.1 The Type System of λ cES . . . . . . . . . . . . . . . . . . 4.2.2 Subject reduction . . . . . . . . . . . . . . . . . . . . . . 4.2.3 Progress . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.3 Termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.3.1 Technical Definitions . . . . . . . . . . . . . . . . . . . . 4.3.2 Strong Normalization for λ cES . . . . . . . . . . . . . . . 4.3.3 Proof of Proposition 4.3.9 . . . . . . . . . . . . . . . . . 4.4 λ C and λ cES . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	Bibliography	153
	Chapter 1

4.4.1 The concurrent λ-calculus λ C . . . . . . . . . . . . . . . 4.4.2 Simulation . . . . . . . . . . . . . . . . . . . . . . . . . . 4.4.3 Adequacy . . . . . . . . . . . . . . . . . . . . . . . . . . 4.5

partition of the set of ports into pairs called w ires. A wire with one (resp.

	rewriting relation is confluent (resp. weakly normalizing, strongly normalizing)
	if all elements t ∈ A are.
	Definition 2.1.2. Simple nets
	Given a countable set, whose elements are called ports, a simple net is given by
	1. A finite set of ports
	2. A finite set of cells. A cell is a finite non-empty sequence of pairwise distinct
	ports, and two cells have pairwise distinct ports. The first port of a cell
	c is called the principal port and written p(c), and the (i + 1)th the ith
	auxiliary port, noted p i (c). The number of auxiliary ports is called the
	arity of the cell. A port is free if it does not occur in a cell.
	3. A labelling of cells by symbols amongst {1, ⊗, `, ?, !, ! p } where p is a strictly
	positive integer. We ask moreover that the arity respects the following
	table:
	Symbol 1 `⊗	?	!	! p
	Arity 0 2 2 0, 1 or 2 0, 1 or 2 p
	4. A

  wire (p 1 , p 2 ) labelled by F is identified with the reversed wire (p 2 , p 1 ) labelled by F ⊥ . must have no floating wires and precisely n ≥ 1 free wires w 1 , . . . , w p . Assuming the orientation to be toward their free port, w 1 is labelled by A and for 1 < i ≤ p, w i is labelled by ?B i .

	6. To each ! p nodes -called an exponential box -is associated a simple net in an inductive manner. Let ! p+1 be a box where the wires attached to its ports (oriented outwards) are labelled by !A, ?B 1 , . . . , ?B p . The associated tensor par dereliction contraction cocontraction weakening coweakening exponential box (! p ) simple net S one Table 2.1: Cells and box

Table 2

 2

		.2: Reduction rules
		? ≡ ?	?	?	≡ ?
					?
		! ≡ !	!	!	≡ !
					!
		Table 2.3: Equivalence relation
	2.2.2 Lifting reduction to nets
	The reduction is lifted to nets by allowing the reduction of an arbitrary number
	of summands at once (Definition 2.2.2). As we consider different summands
	as different results living in parallel universes, this make sense to be able to
	reduces several of them at once.
	Definition 2.2.2. Sum reduction
	Let → a ⊆ S N × P N be a reduction from simple nets to nets. We define the ARS
	(P N , ⇒ a ) by: R ⇒ a	n i T i if
	1. Either S i = T i or S i → a T i
	2. There is at least one i such that S i → a T i
	Definition 2.2.3. The ⇒ reduction on nets

  is the simple net obtained from R by connecting the input i to the output o. Proposition 3.2.3. Let R be a routing area and (i, o)

  1 , v 2 ) where v 1 (resp. v 2 ) is either the cell containing src(w) (resp. tgt(w)), or src(w) (resp. tgt(w)) directly if it is free. We remind that cells, ports, wires, etc. are defined in Definition 2.1.2. Definition 3.3.2. Non bouncing path Let R be a simple net. Let π be a finite sequence (v 1 , e 1 , v 2 , e 2 , . . . , v n , e n , v n+1 )

Table 4 .

 4

	2: Evaluation Contexts

  Thus by induction P and Q are themselves either values, of the form M norm , or a parallel of values and M norm forms. It is immediate that neither P or Q can be of the form M 1 M 2 (they would have to be typed by B and coudn't be applied or applied to), thus P and Q are either values or of the form M norm . Now, if both are values (note that P and Q must be closed terms), the only way for P to have type A

	e 1

  e) (by hypothesis and), and we apply 2. of Lemma 4.3.17.• M = * : * [σ] → * ,and we also apply 2. of Lemma 4.3.17. * is trivially (WB) and (SN). • M = λy.M : M [σ] → λx.(M [σ]). We have α = B e 1 → α . By 2. of Lemma 4.3.17, it suffices to prove that λx.(M [σ]

  has a typing judgement of the formx 1 : A 1 , . . . , x n : A n , y 1 : B 1 , . . . , y m : B m M : (α, e). By induction, τ (y k )[σ] ∈ SC R (B i , ∅). As τ (y k )[σ] → τ (y k ){σ},[START_REF] Accattoli | leftmost-outermost) beta reduction is invariant, indeed[END_REF]. of Lemma 4.3.17, the latter is in SC R (B i , ∅). Thus we can apply the induction hypothesis on M : M [τ, σ] ∈ SC R (α, e).

Table 4 .

 4 4: Structural Rules of λ C

	E ::= [.] | E M | M E
	C ::= [.] | (C P ) | (P C)

Table 4 .

 4 5: Evaluation Contexts of λ C

	Reduction rules

Table 4 .

 4 6: Reduction rules of λ C

  use (Equation (4.2)) with M = E[M ] to get the result.Proof. Theorem 4.4.14 Since P is well-typed, M is well-typed by Proposition 4.4.3. By Theorem 4.3.10, M is strongly normalizing. We can thus proceed by induction on η(M ), the length of the longest reduction starting from M . If η(M ) = 0, i.e. M is a normal form, this is trivially true.

	Lemma 4.4.11 states that explicit substitutions implement implicit substitu-
	tions, up to the substitution order.
	Lemma 4.4.11. Explicit substitution
	Let P = C[E[M [σ]]] with M containing no explicit substitutions nor upward
	reference substitution. Then
	P → * nd P

s C[E[M {V /x}]]

Non-deterministic reduction In the following, we will sometimes not want to deal with the clumsiness of handling sums of terms everywhere. We thus define

Acknowledgements

We use the diagram of Figure 2.6 to get the upper square in the figure below. Then we apply the IH to get the bottom part S :

(a) β-reduction

(b) Variable Substitutions (subst var )

x[σ] → σ(x) if defined, or x otherwise (subst unit )

Congruence case: If M → M by any of the previous rules, then Finally:

Congruence case: If M → M by any of the previous rules, then S[C[E[M ]] → S[C[E[M ]]]

Finally:

(subst-r' )

Table 4.3: Reduction Rules. These are closed under the structural rules of Table 4.1

an alternative non-deterministic reduction, denoted by → nd . If a reduction sequence is seen as a tree, where branching points correspond to (subst-r get ) and the children to all the summands produced by this rule, then a sequence of reductions → nd corresponds to a branch in this tree.

Definition 4.1.9. Non-deterministic reduction of λ cES We define → nd by replacing the (subst-r get ) reduction by the following two rules:

Remark 4.1.10. An alternative approach to λ-substitution would be to make downward substitutions not vanish (i.e. getting rid of Rule (subst-r val )). In this situation, values would be handled with their whole context of references assignment. Apart from the heavy syntactical cost of carrying around a lot of similar and possibly useless substitutions, the idea that hidden effects are released at application appears more natural regarding type and effect systems, as the one we introduce in Section 4.2.

Remark 4.1.11. Rule (subst-r' ) acts as a garbage collection to eliminate top-level upward substitutions. While not necessary, this will greatly ease the statement and proof of lemmas and theorems (such as Lemma 4.2.7).

Weak confluence

As opposed to calculus with implicit substitution, such as the λ-calculus, λ cES may have numerous overlapping redexes, that are often called critical pairs in the literature. Confluence then becomes painful to establish. We prove a weaker property, weak confluence: an ARS (A, →) is weakly confluent if, for any term t ∈ A such that u ← t → u , then there exists v such that u → * v * ← u . The difference with confluence is that in the hypothesis, t is assumed to reduce to u and u in only one step, instead of an arbitrary number of steps. Thanks to the termination theorem proved in Section 4.3, the Newman's lemma will allow us to deduce that the typed fragment is confluent.

Proposition 4.1.12. Weak confluence Let M be a term such that M → M 1 and M → M 2 . Then

To show weak confluence, we just examine all the possible critical pairs of the language. The following lemma classifies the different kind of possible critical pairs:

We define the skeleton of a term Sk(M ) by removing all downward reference substitutions that are not under an abstraction. Definition 4.1.15. Skeleton Let M be a term of λ cES . We define the term Sk(M ) as:

We say that M N if:

• Sk(M ) = Sk(N ), and thus we can put in a one-to-one correspondence the occurrences of get(r) and (M 1 M 2 )[V] λ subterms of M and N

• For all such get(r) occurrences, Reach(get(r), M ) ⊆ Reach(get(r), N )

Similarly, we say that M V N if the difference between reachability sets involved in the definition is somehow "bounded" by V:

• Sk(M ) = Sk(N )

• For all such occurrences of get(r), Reach(get(r),

The relations and V are partial preorders on terms. We write M N when M N and N M .

M M if M and M have the same structure but the available substitutions in scope of each get(r) in M are contained in M ones. Thus, M can do at least everything M can do. The second preorder V controls precisely what the difference between reachability sets can be. The following properties make these explanations formal:

Where Reg R (r) for a reference r is defined by Reg R (r) = {r} ∪ Reg R (R(r), ∅), and is naturally extended to an effect e by Reg R (e) = r∈e Reg R (r). Finally, the region of a type and effect (α, e) is defined as Reg R (α, e) = Reg R (α) ∪ Reg R (e). Remark 4.2.4. Note that we always have Eff R (α, e) ⊆ Reg R (α, e) ⊆ dom(R).

Subject reduction

The language λ cES satisfies the usual safety properties of a typed calculus: subjet reduction and progress. Lemma 4.2.5. Subject reduction Let R; Γ M : (α, e) be a typing judgment, and assume that M → M . Then R; Γ M : (α, e). Remark 4.2.6. The fact that an effectful term may become pure after reduction is reflected by the subtyping relation. For example, consider P = get(r)[V] ↓ where R P : (A, {r}) and P → (V + . . .). Since V is a value it can only be given the type R V : (A, ∅). Subject reduction would however require that V has the same type (A, {r}) as P . The subtyping relation corresponds to effect containment, meaning that the effects appearing in types are an upper bound of the actual effects produced by a term, so that (A, ∅) is a subtype of (A, {r}).

Proof. Lemma 4.2.5 Case analysis on the reduction rule used :

Then one can form the derivation

using the admissibility of generalized weakening.

We just have to remove the (subst-r) rule to get the result :

Proof. Lemma 4.2.7 By recurrence on M. First assume that M is a simple term M :

then there is always a (subst) rule that can be applied whatever M is.

. But then we are back to the previous case. Hence M reduces, and so does M .

(subst -r)

and thus M also reduces. The same applies if Q reduces. Assume now that P → P by (subst-r' ), meaning that P = P [V] ↑ . Then we can apply (subst-r' app-left ) to M . Similarly, we can apply (subst-r' app-right )

The only possible reduction in Λ are either (subst-r) ones (excluding (subst-r get )), or the reduction P → λx.(M [σ]). Assume that Λ has an infinite reduction sequence. As (subst-r) rules alone are strongly normalizing, then the reduction P → (λx.M [σ]) must happen at some point. Similarly, after this reduction, the only possible reductions excluding (subst-r) rules are the

To sum up, an infinite reduction sequence starting from Λ must have the form

We omitted a possible bunch of floating reference substitutions for the sake of readability. Reduction steps verify (∀i :

, thus Λ i 3 is strongly normalizing. This contradicts the fact that the reduction sequence (Λ i ) is infinite. Hence, Λ is strongly normalizing. The (WB) is proved similarly: before producing any upward substitution, Λ must perform the reduction step → i 1 , → i 2 and → i 3 . From there it is bounded by a (WB) term, which implies that it is itself (WB).

Parallel We now treat a case that shows the usage of the (WB) condition. Assume that P = M 1 M 2 . Let Γ = x : A 1 , . . . , x n : A n . Since R; Γ P : (B, e), there exists α 1 , α 2 , e 1 , e 2 such that R; Γ (α 1 , e 1 ), R; Γ M 2 : (α 2 , e 2 ), e 1 ∪e 2 ⊆ e. Take e ⊇ e. By induction, M i ∈ SC R (α i , e ). We will show that M 1 M 2 is strongly normalizing: as in the previous case, the proof that it is well-behaved follows the same technique, and we focus on strong normalization. Note that for some appropriate

n is strongly normalizing. This entails in particular that M i itself is strongly normalizing (see the proof of Lemma 4.3.8).

Let V be a reference substitution of strongly computable terms (whose domain is included in e ), we have to prove that Λ = M 1 M 2 [V] ↓ is strongly normalizing. Assume that Λ has an infinite reduction. The reducts of Λ have the forms

M n 2 → . . . where we omitted possible reference substitutions at the top level. We start by giving an explicit (non inductive) characterization of strongly computable terms: Lemma 4.3.12. Characterization Let

for all U, (V i ) satisfying the above conditions. In the following, we may conveniently omit some of the parameters (M, U, (V i )) of Λ.

Proof. By induction on types.

Then next series of lemmas aims to prove an inclusion relation between strongly computable terms, namely that e ⊆ e =⇒ SC R (α, e) ⊆ SC R (α, e ). This result is stated in Lemma 4.3.16. The idea behind is that adding possible reference substitutions in Λ(M ) for a term M ∈ SC R (α, e) does not change the normalization (or well-behaving), as either these references are already accounted for by some effect in α, or they do not belong to Eff R (α, e) and the corresponding substitutions can not be used at all by M .

The following lemma shows that the effects appearing in the type of a term determine which reference the term may act on. Proof. By induction on the typing derivation.

The following lemma holds the technical content of the proof of Lemma 4.3.16. In Section 4.1.4, we introduced preorders , V for comparing the possible behaviors on terms. We showed in Proposition 4.1.18 that if M N , then everything that can be done by M can be mimicked in N . Here, we prove a converse result in a very specific case. We take a term M V N , and make the additional assumption that for any get(r) in M , r ∈ dom(V ). In others words, V is composed of reference assignments that can never be used by M . In this case, then the converse assertion about behaviors also holds, that is everything that can be done by N can also be done by M , as the additional substitutions in N can not be used for at all. Let V be a reference substitution such that dom(V) ∩ e = ∅. Assume that

Proof. The proof is similar to Proposition 4.1.18: most of the developments are totally symmetric in M and N . The only different case is the case of the (subst-r get ). This means that a get(r)[V, W] ↓ is reduced in N , while only get(r)[W] ↓ can be formed in M . However, by Lemma 4.3.13, r ∈ e, thus the value substitution the first get is V ∈ (V, W)(r) = W(r) by the hypothesis on the domain of V. Then this substitution may also be performed on get(r Proof. The proof is identical to the proof of Corollary 4.1.19.

We can now states our monotonicity property about strongly computable sets. Proof. Using the characterization of Lemma 4.3.12, we must show that any Λ(M, V, (V i )) with V and (V i ) adapted to SC R (α, e ) is (SN) (and (WB) for V = ⊥). Let f = dom(V) \ e, by projecting V on e, we have that Λ(M, V e , (V i ))

By Corollary 4.3.15, so is Λ(M, V, (V i )). The (WB) condition is treated similarly.

The following lemma gives a list of technical properties: Let M be a term and S be a store of λ C . S can be written as

We allow S to be the empty store , in which case V S is the nowhere defined function. We define the translation of M under S by

In fact, M S is the normal form reached from M [V S ] ↓ using only downward structural rules (that is, all (subst-r) rules excepted (subst-r get )). For any program P = M S, we define P = M S . The case where P does not contain any store is considered as if S = .

Since the type systems of λ cES and λ C are very close, the translation preserves the fact of being well-typed: The reduction of λ cES has the limitation of not being able to reduce under abstractions, even to propagate explicit substitutions. The variable substitutions propagation under abstractions will thus be delayed until the corresponding lambda will be applied. To cope with this subtlety, we introduce a relation on terms of λ cES that expresses that a term M is related to N if M is the same as N up to the propagation of pending substitutions frozen under lambdas. If we would allow substitutions to be reduced under lambdas, M would reduces to N . Definition 4.4.4. Substitution relation We define s as :

Where we extended point-wise the definition of s to functions and multisets.

We can now state the simulation result modulo s : Theorem 4.4.5. Simulation Let P, Q be λ C programs such that P → * Q. Then

The following subsection proves Theorem 4.4.5 with the help of auxiliary lemmas.

Proof of Simulation

• . . . The remaining cases are treated similarly, the reduction rules being designed to make this lemma work.

We prove now the main technical result from which the simulation theorem follows easily: Proposition 4.4.12. One-step simulation Let P, Q be λ C programs such that P → Q. Then P → * nd M s Q Proof. Proposition 4.4.12 By case analysis on the reduction rule applied :

Then, by one application of β v in λ cES , we have

We apply Lemma 4.4.9 with to deduce

get We have P = E[get(r)] N S with S = S r ⇐ V , and

The rule (subst-r get ) gives The only missing part is the following lemma allowing us to extend the result of Proposition 4.4.12. It shows that the substitution order is a relation that is compatible with reduction. Lemma 4.4.13. Subsitution order is compatible with reduction

Proof. Lemma 4.4.13 By case analysis on the reduction rule applied in M → nd M . As s only relates to subterms that are under an abstraction, and the reduction do not reduce under abstractions, the reduction and the substitution order do not interact.

Proof. Simulation(Theorem 4.4.5) By induction on the length of the reduction P → * Q, using Proposition 4.4.12 and Lemma 4.4.13.

Adequacy

The adequacy theorem states that the summands of the normal form of M are either the translation of a normal form T = V 1 . . . V n that is a reduct of the original M , or garbage, that is a non-value term that corresponds to execution paths which deadlocked. We can recognize this garbage, thus eliminate it: with this additional operation, the summands of the normal form of M coincide with the values that are reachable by M .

Theorem 4.4.14. Adequacy Let P be a well-typed term of λ C . If P → * i M i such that i M i is a normal form, then for any i, P → * P i with M i s M i P i . That is, any term appearing in the normal form of the translation of P is -bounded (up to the substitution order) by the translation of a reduct of P .

In particular, applied to values, this gives the sought property for λ cES : Corollary 4.4.15. Let P be a well-typed term of λ C . Assume that P → * M + M where M is a normal form.

The only problematic case is the non deterministic reduction (subst-r get ) which creates new summands. The proof consist in showing that these summands are actually limited in what they can do. Formally, they are bounded by the initial term that is being reduced, in the sense of the preorder . The following lemma states that indeed the case of deterministic reduction is trivial: Proof. Lemma 4.4.17 Given the form of a term which is the translation of a λ C term, the only redexes in M are either premises of a (subst-r') rule, the (β v ) rule or the (subst-r get ) rule. In the first case, it corresponds to a reducible set whose reduction can be carried on in M by pushing the upward substitution to the top and pushing down the corresponding generated downward substitutions, to obtain the translation of N (as in the simulation of a (set) reduction). We can proceed the same way with (β v ) : this corresponds to a β-redex in N , where N is the result of reducing it, and M is obtained by pushing down the generated substitutions (variable and references). As we saw in simulation, this gives the desired result but up to s .

Finally, if the reduction rule is (subst-r get ), then either it chose one of the available values and it corresponds exactly to a get reduction N → N , or it threw away available values, in which case N = N , M = M and clearly M N .

Working on the nets

We will see in the following that the translation of a F -normal form has not many possible reductions left. However, a few steps may remain to eventually reach a normal form. The first step is to collect and merge all the routing areas that are created and connected during the translation. Doing so, we separate the net between a part that closely follows the translated term structure, and a big routing area which connects various subterms to enable communication through references between them. Once this is done, a few starving get(r) may interact with the routing area by generating sums, but without being actually substituting. The following definition give the shape obtained after the merging of routing: The translation of term with at least one free variable is separable. The reason is that constructors such as application, substitution, parallel composition, etc. preserve separability. Moreover, the translation of values with free variables are obviously separable. The weakenings, which correspond to free variables, materializes as auxiliary doors of exponential boxes, and block further reduction. Lemma 5.3.5. Open terms separability Let Γ, x : A M : (α, e) a λ cES well-typed term, then its translation M • is separable.

Proof. Lemma 5.3.5 We proceed by induction on terms.

Finally, we can state the separability of normal forms: Lemma 5.3.6. Normal form separability The translation of a F -normal form is separable It is proved as Lemma 5.3.5, by induction on the syntax of F -normal forms. We can eventually prove from this last lemma: Lemma 5.3.7. Termination of λ cES + The translation of a F -normal form is strongly normalizing.

Proof. Lemma 5.3.7 We apply Lemma 5.3.6 to reduce the translation of a F -normal form F to a routing area R connected to S satisfying separability conditions. S and R are normal. The potential redexes must involve a wire at the interface of R and S. The inputs of R are connected to S, either to a par or to the conclusion of an open box and thus can't form any redex with (co)weakenings and (co)contractions of R.

The outputs of R are either connected to the auxiliary port of a tensor, the auxiliary port of a cocontraction or to a dereliction. Only the latter may form a new redex. If the output of R is a coweakening, then everything reduces to 0. If it is just a wire, then the dereliction is connected through this wire to an input of R which again can't be part of any redex. The only remaining case is when the output of R is a cocontraction tree. Then we can perform the non-deterministic ba → reductions, and we go back to exactly the two previous cases as the dereliction is finally connected to a leaf of the tree of an input.

Hence, after we performed finitely many ba → reductions, we finally get a normal form, which is either 0, or a sum of the previous net S connected to simpler routing areas R i .

From this last lemma follows Proposition 5.3.1.

Adequacy

The adequacy theorem states that the summands of the normal form of M • are either the translation of a normal form T = V 1 . . . V n (where V 1 , . . . , V n are values of λ cES ) that is a reduct of the original M , or garbage, that is a non correct net that corresponds to execution paths which deadlocked. We can recognize this garbage, thus eliminate it. With this additional operation, the summands of the normal form of M • coincide with the translation of (parallel of) values that are reachable by M . We stated a similar adequacy theorem between λ C and λ cES (Theorem 4. To check the converse, we have to check that the translations of the remaining M i s (the ones that are not parallel of values) cannot be reduced (as simple nets) to value nets, or do not generate new summands that themselves reduce to value nets. We can extract this fact from the proof of termination (cf Section 5.3.2) that shows that in the translation of a term which is not a value, the only remaining reduction are either the merging of routing areas, a reduction to 0, or a sequence of ba → which conserve the overall structure of a term. In particular, this does not produce any value during its reduction to a normal form in nets.

Summary

In this chapter, we illustrated the use of the tools introduced in Chapter 2 and Chapter 3, a differential net system (Chapter 2) and routing areas (Chapter 3), by constructing an encoding from the concurrent λ-calculus with explicit substitutions λ cES introduced in Chapter 4 in nets.

We use the monadic translation of Tranquilli [START_REF] Tranquilli | Translating types and effects with state monads and linear logic[END_REF] to encode types from the stratified type and effect system to standard formulas of multiplicative LL. We then translate terms as nets, with free wires corresponding both to variables and effect (references). We combine the "pure λ-calculus" part following the standard call-by-value translation in LL [START_REF] Maraist | Call-byname, call-by-value, call-by-need, and the linear lambda calculus[END_REF], and combine the wires corresponding to references through routing areas. These areas are specifically designed to encode the order of the evaluation of effects in λ cES . This provides a modular translation of well-typed term of λ cES in nets.

We then prove a simulation theorem, showing that nets implements the reduction of λ cES . We show that the translation of a term is weakly normalizing. In the section on adequacy, we prove that the values in the normal form of the