8.3. Liste des formules🔗

• Formule 1 : La composition de contextes, définie à partir des deux fonctions de la loi distributive
• Formule 2 : Grammaire des types : trois strates, le grade comme quadruplet, l'effet comme produit d'une quantale et d'une famille temporelle indexée par les niveaux
• Formule 3 : Le prédicat de treillis fini, défini par induction sur la grammaire des types de valeur
• Formule 4 : Grammaire des termes, en style appel par poussée de valeur
• Formule 5 : Le jeu de règles central : variable, adjonction, modalité graduée, effets et sous-typage
• Formule 6 : Règles des modalités « toujours » et « éventuellement », et la perte de borne qu'attendre coûte
• Formule 7 : La forme d'une opération à portée : son effet est une fonction de l'effet de son argument
• Formule 8 : Le monoïde des transformateurs d'effets, ses deux familles de générateurs et ses trois lois
• Formule 9 : Les connecteurs qui suivent les patrons déjà posés
• Formule 10 : Les deux règles du point fixe coinductif. L'observation consomme une unité de taille ; le copatron en produit une.
• Formule 11 : La conjonction additive partage son contexte au lieu de l'additionner, et l'arène le multiplie par sa longueur
• Formule 12 : Séquencement et mise en parallèle du coût, par niveau
• Formule 13 : La mise en parallèle et l'application vectorisée. La profondeur de Vmap ne dépend pas de n.
• Formule 14 : Les canaux de session et les boîtes aux lettres, avec l'algèbre des motifs
• Formule 15 : Engendrer, créer une boîte, émettre, recevoir sous garde, libérer
• Formule 16 : Localiser un calcul, déplacer une valeur, récupérer d'une défaillance
• Formule 17 : La condition sous laquelle la contrainte de complexité peut être répartie sur les deux autres composantes : multiplier une exigence et multiplier l'effet qu'elle traverse sont la même chose
• Formule 18 : Les réductions pures : une par forme d'élimination, chacune consommant l'introduction qui lui correspond
• Formule 19 : Les réductions à effet : la trace s'étend du grade que l'opération déclare
• Formule 20 : La relation logique au niveau \ell, par récurrence sur la grammaire des types : la clause de la modalité graduée est la seule qui décide, les autres se contentent de la propager
• Formule 21 : Les sortes du métalangage : un genre, qui dit à quoi le nom sert, et un niveau, qui dit où ses événements sont observables
• Formule 22 : Le jugement de bon sortage. Les trois premières clauses sont celles du cadre emprunté ; la quatrième est propre à K7PL, dont les motifs de jonction ne relèvent pas de la communication binaire.
• Formule 23 : La relation logique sur les types de session, au niveau \ell. Le niveau du canal décide, comme le niveau du grade décidait sur les valeurs.
• Formule 24 : Typage d'une expansion de macro. Aucune de ses parties n'est nouvelle : le contexte est celui du lemme de substitution, l'effet celui du transport \varphi. Le produit est celui de la quantale, non commutatif : \mathrm{occ}(m) est la suite des occurrences des métavariables dans l'ordre du corps, non l'ensemble des indices i \leq n. \varepsilon_{\mathrm{body}} est l'effet déclaré du code produit hors arguments ; l'effet de l'expansion elle-même, \varepsilon_{\mathrm{exp}} = \mathbf{1}, est un lemme du bac à sable, non une déclaration.