When programs have to watch paint dry. (English) Zbl 07770329
Kupferman, Orna (ed.) et al., Foundations of software science and computation structures. 26th international conference, FOSSACS 2023, held as part of the European joint conferences on theory and practice of software, ETAPS 2023, Paris, France, April 22–27, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13992, 1-23 (2023).
Summary: We explore type systems and programming abstractions for the safe usage of resources. In particular, we investigate how to use types to modularly specify and check when programs are allowed to use their resources, e.g., when programming a robot arm on a production line, it is crucial that painted parts are given enough time to dry before assembly. We capture such temporal resources using a time-graded variant of Fitch-style modal type systems, develop a corresponding modally typed, effectful core calculus, and equip it with a graded-monadic denotational semantics illustrated by a concrete presheaf model. Our calculus also includes graded algebraic effects and effect handlers. They are given a novel temporally aware treatment in which operations’ specifications include their execution times and their continuations know that an operation’s worth of additional time has passed before they start executing, making it possible to safely access further temporal resources in them.
For the entire collection see [Zbl 1524.68006].
For the entire collection see [Zbl 1524.68006].
References:
| [1] | Ahman, D., Bauer, A.: Runners in Action. In: Proc. of 29th European Symp. on Programming, ESOP 2020. Lect. Notes Comput. Sci., vol. 12075, pp. 29-55. Springer (2020) · Zbl 1508.68050 |
| [2] | Ahman, D., Fournet, C., Hritcu, C., Maillard, K., Rastogi, A., Swamy, N.: Recalling a witness: foundations and applications of monotonic state. Proc. ACM Program. Lang. 2(POPL), 65:1-65:30 (2018) |
| [3] | Ahman, D., Pretnar, M., Radešček, J.: Higher-Order Asynchronous Effects (2021), extended abstract presented at the 9th ACM-SIGPLAN Wksh. on Higher-Order Programming with Effects, HOPE 2021 |
| [4] | Atkey, R.: Syntax and Semantics of Quantitative Type Theory. In: Proc. of 33rd Annual ACM/IEEE Symp. on Logic in Computer Science, LICS 2018. pp. 56-65. ACM (2018) · Zbl 1452.03029 |
| [5] | Bahr, P., Grathwohl, H.B., Møgelberg, R.E.: The clocks are ticking: No more delays! In: Proc. of 32nd Annual ACM/IEEE Symp. on Logic in Computer Science, LICS 2017. pp. 1-12. IEEE Computer Society (2017) · Zbl 1452.03031 |
| [6] | Bahr, P., Graulund, C., Møgelberg, R.E.: Simply RaTT: a fitch-style modal calculus for reactive programming without space leaks. Proc. ACM Program. Lang. 3(ICFP), 109:1-109:27 (2019) |
| [7] | Barendregt, H., Dekkers, W., Statman, R.: Lambda Calculus with Types. Cambridge University Press (2013) · Zbl 1347.03001 |
| [8] | Bauer, A.: What is algebraic about algebraic effects and handlers? CoRR abs/1807.05923 (2018) |
| [9] | Bauer, A., Pretnar, M.: Programming with algebraic effects and handlers. J. Log. Algebr. Meth. Program. 84(1), 108-123 (2015) · Zbl 1304.68025 |
| [10] | Beck, J.M.: Triples, algebras and cohomology. Reprints in Theory and Applications of Categories (2), 1-59 (2003), Note: Originally published as: Ph.D. thesis, Columbia University, 1967 · Zbl 1022.18004 |
| [11] | Benton, N., Bierman, G.M., de Paiva, V., Hyland, M.: Linear lambda-calculus and categorial models revisited. In: Selected Papers from Computer Science Logic, CSL ’92. Lect. Notes Comput. Sci., vol. 702, pp. 61-84. Springer (1992) · Zbl 0840.03003 |
| [12] | Bierman, G.M., de Paiva, V.: On an Intuitionistic Modal Logic. Studia Logica 65(3), 383-416 (2000) · Zbl 0963.03033 |
| [13] | Birkedal, L., Clouston, R., Mannaa, B., Møgelberg, R.E., Pitts, A.M., Spitters, B.: Modal dependent type theory and dependent right adjoints. Math. Struct. Comput. Sci. 30(2), 118-138 (2020) · Zbl 1479.03011 |
| [14] | Bizjak, A., Grathwohl, H.B., Clouston, R., Møgelberg, R.E., Birkedal, L.: Guarded Dependent Type Theory with Coinductive Types. In: Proc. of 19th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2016. Lect. Notes Comput. Sci., vol. 9634, pp. 20-35. Springer (2016) · Zbl 1475.68060 |
| [15] | Borghuis, V.: Coming to terms with modal logic: on the interpretation of modalities in typed lambda-calculus. Ph.D. thesis, Mathematics and Computer Science, Technische Universiteit Eindhoven (1994) · Zbl 0811.03010 |
| [16] | Brunel, A., Gaboardi, M., Mazza, D., Zdancewic, S.: A Core Quantitative Coeffect Calculus. In: Proc. of 23rd European Symp. on Programming, ESOP 2014. Lect. Notes Comput. Sci., vol. 8410, pp. 351-370. Springer (2014) · Zbl 1405.68074 |
| [17] | Carboni, A., Johnstone, P.: Connected limits, familial representability and artin glueing. Math. Struct. Comput. Sci. 5(4), 441-459 (1995) · Zbl 0849.18002 |
| [18] | Cave, A., Ferreira, F., Panangaden, P., Pientka, B.: Fair reactive programming. In: Proc. of 41st Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 2014. pp. 361-372. ACM (2014) · Zbl 1284.68127 |
| [19] | Clouston, R.: Fitch-Style Modal Lambda Calculi. In: Proc. of 21st Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2018. Lect. Notes Comput. Sci., vol. 10803, pp. 258-275. Springer (2018) · Zbl 1504.03014 |
| [20] | Convent, L., Lindley, S., McBride, C., McLaughlin, C.: Doo bee doo bee doo. J. Funct. Program. 30, e9 (2020) · Zbl 1442.68026 |
| [21] | Dolan, S., Eliopoulos, S., Hillerström, D., Madhavapeddy, A., Sivaramakrishnan, K.C., White, L.: Concurrent System Programming with Effect Handlers. In: Trends in Functional Programming. pp. 98-117. Springer (2018) |
| [22] | Fujii, S., Katsumata, S., Melliès, P.: Towards a Formal Theory of Graded Monads. In: Proc. of 19th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2016. Lect. Notes Comput. Sci., vol. 9634, pp. 513-530. Springer (2016) · Zbl 1474.18011 |
| [23] | Gaboardi, M., Katsumata, S., Orchard, D.A., Breuvart, F., Uustalu, T.: Combining effects and coeffects via grading. In: Proc. of 21st ACM SIGPLAN Int. Conf. on Functional Programming, ICFP 2016. pp. 476-489. ACM (2016) · Zbl 1361.68037 |
| [24] | Ghica, D.R., Smith, A.I.: Bounded Linear Types in a Resource Semiring. In: Proc. of 23rd European Symp. on Programming, ESOP 2014. Lect. Notes Comput. Sci., vol. 8410, pp. 331-350. Springer (2014) · Zbl 1405.68059 |
| [25] | Girard, J.Y.: Linear logic. Theor. Comput. Sci. 50(1), 1-101 (1987) · Zbl 0625.03037 |
| [26] | Gratzer, D.: Normalization for multimodal type theory. In: Proc. of 37th Annual ACM/IEEE Symp. on Logic in Comp. Sci., LICS 2022. pp. 2:1-2:13. ACM (2022) |
| [27] | Gratzer, D., Cavallo, E., Kavvos, G.A., Guatto, A., Birkedal, L.: Modalities and parametric adjoints. ACM Trans. Comput. Logic 23(3) (2022) · Zbl 1505.03030 |
| [28] | Gratzer, D., Kavvos, G.A., Nuyts, A., Birkedal, L.: Multimodal dependent type theory. Log. Methods Comput. Sci. 17(3) (2021) · Zbl 1498.03030 |
| [29] | Haller, P., Prokopec, A., Miller, H., Klang, V., Kuhn, R., Jovanovic, V.: Scala documentation: Futures and promises (October 2022), available online at https://docs.scala-lang.org/overviews/core/futures.html |
| [30] | Honda, K., Vasconcelos, V., Kubo, M.: Language Primitives and Type Discipline for Structured Communication-Based Programming. In: Proc. of 7th European Symp. on Programming, ESOP 1998. Lect. Notes Comput. Sci., vol. 1381, pp. 122-138. Springer (1998) |
| [31] | Hyland, M., Plotkin, G., Power, J.: Combining effects: Sum and tensor. Theor. Comput. Sci. 357(1-3), 70-99 (2006) · Zbl 1096.68088 |
| [32] | Jeltsch, W.: Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming. In: Proc. of the 28th Conf. on the Mathematical Foundations of Programming Semantics, MFPS 2012. ENTCS, vol. 286, pp. 229-242. Elsevier (2012) · Zbl 1342.68051 |
| [33] | Jeltsch, W.: Abstract categorical semantics for resourceful functional reactive programming. J. Log. Algebraic Methods Program. 85(6), 1177-1200 (2016) · Zbl 1353.68043 |
| [34] | Jung, R., Krebbers, R., Jourdan, J., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, e20 (2018) · Zbl 1476.68062 |
| [35] | Katsumata, S.: Parametric effect monads and semantics of effect systems. In: Proc. of 41st Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 2014. pp. 633-646. ACM (2014) · Zbl 1284.68133 |
| [36] | Katsumata, S., McDermott, D., Uustalu, T., Wu, N.: Flexible presentations of graded monads. Proc. ACM Program. Lang. 6(ICFP), 902-930 (2022) |
| [37] | Kavvos, G.A.: The Many Worlds of Modal \(\lambda \)-calculi: I. Curry-Howard for Necessity, Possibility and Time. CoRR abs/1605.08106 (2016) |
| [38] | Kelly, G.: Basic Concepts of Enriched Category Theory. No. 64 in Lecture Notes in Mathematics, Cambridge University Press (1982) · Zbl 0478.18005 |
| [39] | Kock, A.: Strong functors and monoidal monads. Archiv der Mathematik 23(1), 113-120 (1972) · Zbl 0253.18007 |
| [40] | Koopman, P., Fokker, J., Smetsers, S., van Eekelen, M., Plasmeijer, R.: Functional Programming in Clean. University of Nijmegen (1998), draft |
| [41] | Kripke, S.A.: Semantical Analysis of Modal Logic I. Normal Propositional Calculi. Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 9(5-6), 67-96 (1963) · Zbl 0118.01305 |
| [42] | Krishnaswami, N.R.: Higher-order functional reactive programming without spacetime leaks. In: Proc. of 18th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP 2013. pp. 221-232. ACM (2013) · Zbl 1323.68128 |
| [43] | Leijen, D.: Algebraic Effect Handlers with Resources and Deep Finalization. Tech. Rep. MSR-TR-2018-10, Microsoft Research (April 2018) |
| [44] | Levy, P.B., Power, J., Thielecke, H.: Modelling environments in call-by-value programming languages. Inf. Comput. 185(2), 182-210 (2003) · Zbl 1069.68073 |
| [45] | Mac Lane, S.: Categories for the Working Mathematician. No. 5 in Graduate Texts in Mathematics, Springer-Verlag (1971) · Zbl 0232.18001 |
| [46] | Mac Lane, S., Moerdijk, I.: Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Universitext, Springer (1992) · Zbl 0822.18001 |
| [47] | Mannaa, B., Møgelberg, R.E.: The Clocks They Are Adjunctions Denotational Semantics for Clocked Type Theory. In: Proc. of 3rd Int. Conf. on Formal Structures for Computation and Deduction, FSCD 2018. LIPIcs, vol. 108, pp. 23:1-23:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018) · Zbl 1462.68023 |
| [48] | Martini, S., Masini, A.: A Computational Interpretation of Modal Proofs, pp. 213-241. Springer Netherlands (1996) · Zbl 0867.03016 |
| [49] | McBride, C.: I Got Plenty o’ Nuttin’. In: A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. Lect. Notes Comput. Sci., vol. 9600, pp. 207-233. Springer (2016) · Zbl 1333.68014 |
| [50] | McDermott, D., Uustalu, T.: Flexibly Graded Monads and Graded Algebras. In: Proc. of 14th Int. Conf. on Mathematics of Program Construction, MPC 2022. Lect. Notes Comput. Sci., vol. 13544, pp. 102-128. Springer (2022) · Zbl 07705359 |
| [51] | Melliès, P.A.: Parametric Monads and Enriched Adjunctions (2012), manuscript. https://www.irif.fr/ mellies/tensorial-logic/8-parametric-monads-and-enriched-adjunctions.pdf |
| [52] | Moggi, E.: Computational Lambda-Calculus and Monads. In: Proc. of 4th Ann. Symp. on Logic in Computer Science, LICS 1989. pp. 14-23. IEEE (1989) · Zbl 0716.03007 |
| [53] | Moon, B., Eades III, H., Orchard, D.: Graded Modal Dependent Type Theory. In: Proc. of 30th European Symp. on Programming, ESOP 2021. Lect. Notes Comput. Sci., vol. 12648, pp. 462-490. Springer (2021) · Zbl 1473.68052 |
| [54] | Murphy VII, T.: Modal Types for Mobile Code. Ph.D. thesis, School of Computer Science, Carnegie Mellon University (2008) |
| [55] | Nakano, H.: A Modality for Recursion. In: Proc. of 15th Annual IEEE Symp. on Logic in Computer Science, LICS 2000. pp. 255-266. IEEE Computer Society (2000) |
| [56] | Nanevski, A., Morrisett, G., Birkedal, L.: Hoare type theory, polymorphism and separation. J. Funct. Program. 18(5-6), 865-911 (2008) · Zbl 1155.68354 |
| [57] | Petricek, T., Orchard, D.A., Mycroft, A.: Coeffects: Unified Static Analysis of Context-Dependence. In: Proc. of 40th International Colloquium on Automata, Languages, and Programming, ICALP 2013. Lect. Notes Comput. Sci., vol. 7966, pp. 385-397. Springer (2013) · Zbl 1334.68049 |
| [58] | Petricek, T., Orchard, D.A., Mycroft, A.: Coeffects: a calculus of context-dependent computation. In: Proc. of 19th ACM SIGPLAN Int. Conf. on Functional Programming,ICFP 2014. pp. 123-135. ACM (2014) · Zbl 1345.68069 |
| [59] | Plotkin, G., Power, J.: Algebraic Operations and Generic Effects. Appl. Categor. Struct. (1), 69-94 (2003) · Zbl 1023.18006 |
| [60] | Plotkin, G.D., Power, J.: Notions of Computation Determine Monads. In: Proc. of 5th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2002. Lect. Notes Comput. Sci., vol. 2303, pp. 342-356. Springer (2002) · Zbl 1077.68676 |
| [61] | Plotkin, G.D., Pretnar, M.: Handling Algebraic Effects. Log. Methods Comput. Sci. 9(4:23) (2013) · Zbl 1314.68191 |
| [62] | Prawitz, D.: Natural Deduction: A Proof-Theoretical Study. Almquist and Wiksell (1965) · Zbl 0173.00205 |
| [63] | Radešček, J.: Asinhroni algebrajski učinki. Master’s thesis, Faculty of Mathematics and Physics, University of Ljubljana (2021) |
| [64] | Reynolds, J.C.: Separation Logic: A Logic for Shared Mutable Data Structures. In: Proc. of 17th IEEE Symp. on Logic in Computer Science, LICS 2002. pp. 55-74. IEEE Computer Society (2002) |
| [65] | Schwinghammer, J.: A Concurrent Lambda-Calculus with Promises and Futures. Master’s thesis, Programming Systems Lab, Universität des Saarlandes (2002) |
| [66] | Simpson, A.: The Proof Theory and Semantics of Intuitionistic Modal Logic. Ph.D. thesis, University of Edinburgh (1994) |
| [67] | Smirnov, A.L.: Graded monads and rings of polynomials. J. Math. Sci. 151(3), 3032-3051 (2008) · Zbl 1288.18009 |
| [68] | The Agda Team: The Agda Wiki. Available at https://wiki.portal.chalmers.se/agda/pmwiki.php (2022) |
| [69] | Valliappan, N., Ruch, F., Cortiñas, C.T.: Normalization for Fitch-style modal calculi. Proc. ACM Program. Lang. 6(ICFP), 772-798 (2022) |
| [70] | Wadler, P.: Propositions as sessions. J. Funct. Program. 24(2-3), 384-418 (2014) · Zbl 1307.68025 |
| [71] | Weber, M.: Familial 2-functors and parametric right adjoints. Theory Appl. Categories 18(22), 665-732 (2007) · Zbl 1152.18005 |
| [72] | Wickline, P., Lee, P., Pfenning, F., Davies, R.: Modal Types as Staging Specifications for Run-Time Code Generation. ACM Comput. Surv. 30(3es), 8 (1998) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
