K7PL

1.5. Table normative des symboles🔗

Ce document emploie un symbole par objet, et un objet par symbole. La table 5 en fixe la correspondance, et elle est normative : aucune section ultérieure n'introduit de variante locale, et un symbole absent de cette table n'a pas de sens dans ce document. Une table descriptive documenterait la divergence ; celle-ci l'interdit. RMQ 13. La distinction entre \Delta et \Gamma est celle qui coûte le plus cher à enfreindre : elle sépare ce que le langage exige de ce que la métathéorie manipule.

Tableau 5 :

Les symboles du document et l'objet que chacun dénote

Symbole

Objet dénoté

\Delta

contexte gradué du jugement K7PL

\Gamma

contexte catégorique ou métathéorique, jamais une zone du jugement

\mathcal{R}

semi-anneau ordonné des grades

r,\ q

grades individuels

\mathbb{N}_\infty

conaturels, sous-semi-anneau bien fondé où vivent les indices de taille

M,\ I(M),\ F_M

mode, intervalle admissible, fragment engendré

A,\ B,\ C

types

t,\ c

termes, calculs

\varepsilon,\ \mathcal{E}

effet individuel, effet composé

\mathcal{X}

ensemble d'échappatoires de la divulgation délimitée

\sqsubseteq

ordre de précision de l'information

\preccurlyeq

sous-typage modal, produit mixte sur les quatre composantes

\varphi_r,\ \psi_r

action du grade sur l'effet, sur le contexte

\Delta_1 + \Delta_2

addition ponctuelle de contextes

\boxtimes_\varepsilon

composition de contextes sous effet

A \otimes B

tenseur de types, constructeur du langage

\otimes_{\mathcal{C}}

tenseur de la catégorie ambiante, qui dénote la disjonction de ressources

\ell,\ \hat\ell

niveau de lecture (troisième composante d'un grade) ; niveau de production (indice de la famille d'un effet)

!_r

modalité de ressource

\bigcirc,\ \Box,\ \Diamond

modalités temporelles — délai, permanence, éventualité

\llbracket - \rrbracket

traduction vers le métalangage

Un mot sur le partage des glyphes modaux, car deux relectures indépendantes l'ont demandé en sens contraires. La ressource porte ! et non \Box : c'est le glyphe de l'exponentielle depuis Girard, un lecteur le reconnaît sans l'apprendre, et il ne se confond avec rien. Le carré reste au temps, où la nécessité modale lui donne son meilleur titre. Ce document a longtemps écrit les deux pour le même objet — l'exponentielle ici, le carré indicé aux règles de typage —, ce qui était le vrai défaut, l'un ou l'autre valant mieux que les deux.

Références
  1. MUNCH-MACCAGNONI, Guillaume. Resource Polymorphism [en ligne]. 2018, p. 1–62 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.48550/ARXIV.1803.02796
  2. LORENZEN, Anton; WHITE, Leo; DOLAN, Stephen; EISENBERG, Richard A.; LINDLEY, Sam. Oxidizing OCaml with Modal Memory Management. Proceedings of the ACM on Programming Languages [en ligne]. 2024, vol. 8, no. ICFP, p. 485–514 [visité le 2025-05-08]. Disp. à l’adr. DOI: 10.1145/3674642
  3. ATKEY, Robert. Syntax and Semantics of Quantitative Type Theory. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science [en ligne]. Oxford United Kingdom: ACM, 2018, p. 56–65 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1145/3209108.3209189
  4. MOON, Benjamin; EADES III, Harley; ORCHARD, Dominic. Graded Modal Dependent Type Theory. Programming Languages and Systems [en ligne]. Cham: Springer International Publishing, 2021, vol. 12648, p. 462–490 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1007/978-3-030-72019-3_17
  5. CHOUDHURY, Pritam; EADES, Harley; WEIRICH, Stephanie. A Dependent Dependency Calculus. Programming Languages and Systems [en ligne]. Cham: Springer International Publishing, 2022, vol. 13240, p. 403–430 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1007/978-3-030-99336-8_15
  6. LIU, Yiyun; CHAN, Jonathan; WEIRICH, Stephanie. Consistency of a Dependent Calculus of Indistinguishability. Proceedings of the ACM on Programming Languages [en ligne]. 2025, vol. 9, no. POPL, p. 183–209 [visité le 2025-05-19]. Disp. à l’adr. DOI: 10.1145/3704843
  7. DORÉ, Maximilian. Dependent Multiplicities in Dependent Linear Type Theory [en ligne]. 2025, p. 1–13 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1145/3747531
  8. ORCHARD, Dominic; LIEPELT, Vilem-Benjamin; EADES III, Harley. Quantitative Program Reasoning with Graded Modal Types. Proceedings of the ACM on Programming Languages [en ligne]. 2019, vol. 3, no. ICFP, p. 1–30 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1145/3341714
  9. BRODAL, Gerth Stølting; OKASAKI, Chris. Optimal Purely Functional Priority Queues. Journal of Functional Programming [en ligne]. 1996, vol. 6, no. 6, p. 839–857 [visité le 2025-05-15]. Disp. à l’adr. DOI: 10.1017/S095679680000201X
  10. APPEL, Andrew W. A Critique of Standard ML. Journal of Functional Programming [en ligne]. 1993, vol. 3, no. 4, p. 391–429 [visité le 2025-05-15]. Disp. à l’adr. DOI: 10.1017/S0956796800000836
  11. CHONG, Stephen. Required Information Release. In: 2010 23rd IEEE Computer Security Foundations Symposium [en ligne]. Edinburgh, United Kingdom: IEEE, 2010, p. 215–227 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1109/CSF.2010.22
  12. RAJANI, Vineet; COLEMAN, Alex; KANABAR, Hrutvik. A Graded Modal Approach to Relaxed Semantic Declassification. In: CSF [en ligne]. Santa Cruz, CA, USA: IEEE, 2025, p. 268–283. Disp. à l’adr. DOI: 10.1109/CSF64896.2025.00032
  13. OKASAKI, Chris. Purely Functional Data Structures [en ligne]. s. d.. Disp. à l’adr. DOI: 10.1017/CBO9780511530104
  14. BROWN, James A. A Development of APL2 Syntax. IBM Journal of Research and Development [en ligne]. 1985, vol. 29, no. 1, p. 37–48 [visité le 2025-04-18]. Disp. à l’adr. DOI: 10.1147/rd.291.0037
  15. HUDAK, Paul; HUGHES, John; PEYTON JONES, Simon; WADLER, Philip. A History of Haskell: Being Lazy with Class. In: Proceedings of the Third ACM SIGPLAN Conference on History of Programming Languages [en ligne]. San Diego California: ACM, 2007 [visité le 2025-05-07]. Disp. à l’adr. DOI: 10.1145/1238844.1238856
  16. REYNOLDS, John C. GEDANKEN - a Simple Typeless Language Based on the Principle of Completeness and the Reference Concept. Communications of the ACM [en ligne]. 1970, vol. 13, no. 5, p. 308–319 [visité le 2025-04-18]. Disp. à l’adr. DOI: 10.1145/362349.362364
  17. PRATT, Vaughan R. Transition and Cancellation in Concurrency and Branching Time. Mathematical Structures in Computer Science [en ligne]. 2003, vol. 13, no. 4, p. 485–529 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1017/S0960129503004031
  18. CASTELLAN, Simon; CLAIRAMBAULT, Pierre. The Geometry of Causality: Multi-Token Geometry of Interaction and Its Causal Unfolding. Proceedings of the ACM on Programming Languages [en ligne]. 2023, vol. 7, p. 689–717 [visité le 2025-05-07]. Disp. à l’adr. DOI: 10.1145/3571217
  19. LIEPELT, Vilem; MARSHALL, Danielle; ORCHARD, Dominic. Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types. Proceedings of the ACM on Programming Languages [en ligne]. 2026, vol. 10, p. 721–750 [visité le 2026-08-27]. Disp. à l’adr. DOI: 10.1145/3828697
  20. GORDON, Colin S. Polymorphic Iterable Sequential Effect Systems. ACM Transactions on Programming Languages and Systems [en ligne]. 2021, vol. 43, no. 1, p. 1–79 [visité le 2025-07-02]. Disp. à l’adr. DOI: 10.1145/3450272
  21. MATACHE, Cristina; LINDLEY, Sam; MOSS, Sean; STATON, Sam; WU, Nicolas; YANG, Zhixuan. Scoped Effects, Scoped Operations, and Parameterized Algebraic Theories. ACM Transactions on Programming Languages and Systems [en ligne]. 2025, vol. 47, no. 2, p. 1–33 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1145/3731678
  22. VAN DER REST, Cas; BACH, Casper. Hefty Algebras: Modular Elaboration of Higher-Order Effects. Journal of Functional Programming [en ligne]. 2025, vol. 35, p. e25 [visité le 2026-08-27]. Disp. à l’adr. DOI: 10.1017/S0956796825100142
  23. LINDLEY, Sam; MATACHE, Cristina; MOSS, Sean; STATON, Sam; WU, Nicolas; YANG, Zhixuan. Scoped Effects as Parameterized Algebraic Theories. In: WEIRICH, Stephanie (éd.). Programming Languages and Systems [en ligne]. Cham: Springer Nature Switzerland, 2024, vol. 14576, p. 3–21 [visité le 2026-08-27]. Disp. à l’adr. DOI: 10.1007/978-3-031-57262-3_1
  24. DE VILHENA, Paulo Emílio; POTTIER, François. A Separation Logic for Effect Handlers. Proceedings of the ACM on Programming Languages [en ligne]. 2021, vol. 5, p. 1–28 [visité le 2025-05-07]. Disp. à l’adr. DOI: 10.1145/3434314
  25. JAKE FECHER. Algebraic Effects, Ownership, and Borrowing [en ligne]. Ante, 2024. Disp. à l’adr. https://antelang.org/
  26. GABOARDI, Marco; KATSUMATA, Shin-ya; ORCHARD, Dominic; BREUVART, Flavien; UUSTALU, Tarmo. Combining Effects and Coeffects via Grading. In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming [en ligne]. Nara Japan: ACM, 2016, p. 476–489 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1145/2951913.2951939
  27. LI, Yongming; PEDRYCZ, Witold. Fuzzy Finite Automata and Fuzzy Regular Expressions with Membership Values in Lattice-Ordered Monoids. Fuzzy Sets and Systems [en ligne]. 2005, vol. 156, no. 1, p. 68–92 [visité le 2026-08-19]. Disp. à l’adr. DOI: 10.1016/j.fss.2005.04.004
  28. MANNUCCI, Mirco A.; THURO, Corey. Resource-Bounded Type Theory: Compositional Cost Analysis via Graded Modalities. arXiv.org [en ligne]. 2025, vol. abs/2512.6952, p. 1–20 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.48550/arXiv.2512.06952
  29. CAPORASO, Salvatore; COVINO, Emanuele; PANI, Giovanni. A Predicative Approach to the Classification Problem. Journal of Functional Programming [en ligne]. 2001, vol. 11, no. 1, p. 95–116 [visité le 2025-05-15]. Disp. à l’adr. DOI: 10.1017/S0956796800003853
  30. ATKEY, Robert. Polynomial Time and Dependent Types. Proceedings of the ACM on Programming Languages [en ligne]. 2024, vol. 8, no. POPL, p. 2288–2317 [visité le 2025-06-05]. Disp. à l’adr. DOI: 10.1145/3632918
  31. GHICA, Dan R.; SMITH, Alex I. Bounded Linear Types in a Resource Semiring. In: SHAO, Zhong (éd.). European Symposium on Programming [en ligne]. Berlin, Heidelberg: Springer Berlin Heidelberg, 2014, vol. 8410, p. 331–350 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1007/978-3-642-54833-8_18
  32. TORCZON, Cassia; SUÁREZ ACEVEDO, Emmanuel; AGRAWAL, Shubh; VELEZ-GINORIO, Joey; WEIRICH, Stephanie. Effects and Coeffects in Call-by-Push-Value. Proceedings of the ACM on Programming Languages [en ligne]. 2024, vol. 8, no. OOPSLA2, p. 1108–1134 [visité le 2025-05-08]. Disp. à l’adr. DOI: 10.1145/3689750
  33. KURA, Satoshi; GABOARDI, Marco; SEKIYAMA, Taro; UNNO, Hiroshi. A Category-Theoretic Framework for Dependent Effect Systems [en ligne]. 2026, p. 1–75 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1007/978-3-032-22720-1_15
  34. ÇIÇEK, E.; GABOARDI, M.; GARG, D. Cost-Analysis: How Do Monads and Comonads Differ?. 2016.
  35. AZEVEDO DE AMORIM, P. H. The Compositional Essence of Effectful Cost Analyses: Categorical Foundations and Fibered Logical Relations. Univ. of Bath, s. d..
  36. SAINATI, Daniel; CUTLER, Joseph W.; PIERCE, Benjamin C.; WEIRICH, Stephanie. Typing Strictness. Proc. ACM Program. Lang. [en ligne]. 2026, vol. 10, no. POPL, p. 413–443 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1145/3776657
  37. DOWNEN, Paul; ARIOLA, Zena M. Classical (Co)Recursion: Mechanics. Journal of Functional Programming [en ligne]. 2023, vol. 33, p. e4 [visité le 2025-05-19]. Disp. à l’adr. DOI: 10.1017/S0956796822000168
  38. CHIRIMAR, Jawahar; GUNTER, Carl A.; RIECKE, Jon G. Reference Counting as a Computational Interpretation of Linear Logic. Journal of Functional Programming [en ligne]. 1996, vol. 6, no. 2, p. 195–244 [visité le 2025-05-15]. Disp. à l’adr. DOI: 10.1017/S0956796800001660
  39. SERGEY, Ilya; VYTINIOTIS, Dimitrios; JONES, Simon L. Peyton; BREITNER, Joachim. Modular, Higher Order Cardinality Analysis in Theory and Practice. Journal of Functional Programming [en ligne]. 2017, vol. 27, p. e11 [visité le 2025-05-19]. Disp. à l’adr. DOI: 10.1017/S0956796817000016
  40. PÉDROT, Pierre-Marie; TABAREAU, Nicolas. The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects. Proceedings of the ACM on Programming Languages [en ligne]. 2020, vol. 4, p. 1–28 [visité le 2025-05-05]. Disp. à l’adr. DOI: 10.1145/3371126
  41. BRACHTHÄUSER, Jonathan Immanuel; SCHUSTER, Philipp; OSTERMANN, Klaus. Effects as Capabilities: Effect Handlers and Lightweight Effect Polymorphism. Proceedings of the ACM on Programming Languages [en ligne]. 2020, vol. 4, p. 1–30 [visité le 2025-05-06]. Disp. à l’adr. DOI: 10.1145/3428194
  42. SCHUSTER, Philipp; BRACHTHÄUSER, Jonathan Immanuel; OSTERMANN, Klaus. Compiling Effect Handlers in Capability-Passing Style. Proceedings of the ACM on Programming Languages [en ligne]. 2020, vol. 4, p. 1–28 [visité le 2025-04-30]. Disp. à l’adr. DOI: 10.1145/3408975
  43. VÁKÁR, Matthijs. A Framework for Dependent Types and Effects [en ligne]. Version 2. 2015 [visité le 2026-08-27]. Disp. à l’adr. DOI: 10.48550/ARXIV.1512.08009
  44. NIU, Yue; STERLING, Jonathan; GRODIN, Harrison; HARPER, Robert. A Cost-Aware Logical Framework. Proc. ACM Program. Lang. [en ligne]. 2021, vol. 6, no. POPL, p. 1–31 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1145/3498670
  45. KAVVOS, G. A. The Many Worlds of Modal λ-Calculi: I. Curry-howard for Necessity, Possibility and Time [en ligne]. 2016, p. 1–34 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.48550/ARXIV.1605.08106
  46. ALTENKIRCH, Thorsten; MORRIS, Peter. Indexed Containers. In: 2009 24th Annual IEEE Symposium on Logic In Computer Science [en ligne]. Los Angeles, California, USA: IEEE, 2009, p. 277–285 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1109/LICS.2009.33
  47. OLIVEIRA VALE, Arthur; MELLIÈS, Paul-André; SHAO, Zhong; KOENIG, Jérémie; STEFANESCO, Léo. Layered and Object-Based Game Semantics. In: Proceedings of the ACM on Programming Languages [en ligne]. 2022, vol. 6, no. POPL, p. 1–32 [visité le 2026-08-02]. Disp. à l’adr. DOI: 10.1145/3498703
  48. CHOUDHURY, Vikraman; KRISHNASWAMI, Neel. Recovering Purity with Comonads and Capabilities. Proceedings of the ACM on Programming Languages [en ligne]. 2020, vol. 4, p. 1–28 [visité le 2025-04-30]. Disp. à l’adr. DOI: 10.1145/3408993
  49. COLCOMBET, Thomas; PETRISAN, Daniela. Automata in the Category of Glued Vector Spaces. LIPIcs, Volume 83, MFCS 2017 [en ligne]. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017, vol. 83, p. 52:1-52:14 [visité le 2026-08-27]. Disp. à l’adr. DOI: 10.4230/LIPICS.MFCS.2017.52
  50. The Unicode® Standard. Version 17.0. Unicode, Inc., 2025.