Time warps, from algebra to algorithms. (English) Zbl 07670526
Fahrenberg, Uli (ed.) et al., Relational and algebraic methods in computer science. 19th international conference, RAMiCS 2021, Marseille, France, November 2–5, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13027, 309-324 (2021).
Summary: Graded modalities have been proposed in recent work on programming languages as a general framework for refining type systems with intensional properties. In particular, continuous endomaps of the discrete time scale, or time warps, can be used to quantify the growth of information in the course of program execution. Time warps form a complete residuated lattice, with the residuals playing an important role in potential programming applications. In this paper, we study the algebraic structure of time warps, and prove that their equational theory is decidable, a necessary condition for their use in real-world compilers. We also describe how our universal-algebraic proof technique lends itself to a constraint-based implementation, establishing a new link between universal algebra and verification technology.
For the entire collection see [Zbl 1507.68032].
For the entire collection see [Zbl 1507.68032].
MSC:
| 68Qxx | Theory of computing |
Keywords:
residuated lattices; universal algebra; decision procedures; graded modalities; type systems; programming languagesReferences:
| [1] | Backus, J.W., et al.: The FORTRAN automatic coding system. In: Astrahan, M.M. (ed.) Proceedings of IRE-AIEE-ACM 1957 (Western), pp. 188-198. ACM (1957) |
| [2] | Birkedal, L.; Møgelberg, RE; Schwinghammer, J.; Støvring, K., First steps in synthetic guarded domain theory: step-indexing in the topos of trees, Log. Methods Comput. Sci., 8, 4, 55-64 (2012) · Zbl 1269.03035 · doi:10.2168/LMCS-8(4:1)2012 |
| [3] | Blount, K.; Tsinakis, C., The structure of residuated lattices, Int. J. Algebr. Comput., 13, 4, 437-461 (2003) · Zbl 1048.06010 · doi:10.1142/S0218196703001511 |
| [4] | Bradley, AR; Manna, Z.; Sipma, HB; Emerson, EA; Namjoshi, KS, What’s decidable about arrays?, Verification, Model Checking, and Abstract Interpretation, 427-442 (2005), Heidelberg: Springer, Heidelberg · Zbl 1176.68116 · doi:10.1007/11609773_28 |
| [5] | Caspi, P., Pouzet, M.: Synchronous Kahn networks. In: Proceedings of ICFP 1996, pp. 226-238. ACM (1996) · Zbl 1344.68049 |
| [6] | Colacito, A., Galatos, N., Metcalfe, G., Santschi, S.: From distributive \(\ell \)-monoids to \(\ell \)-groups, and back again (2021). https://arxiv.org/pdf/2103.00146 |
| [7] | Fujii, S.; Katsumata, S.; Melliès, P-A; Jacobs, B.; Löding, C., Towards a formal theory of graded monads, Foundations of Software Science and Computation Structures, 513-530 (2016), Heidelberg: Springer, Heidelberg · Zbl 1474.18011 · doi:10.1007/978-3-662-49630-5_30 |
| [8] | Gaboardi, M., Katsumata, S.Y., Orchard, D., Breuvart, F., Uustalu, T.: Combining effects and coeffects via grading. ACM SIGPLAN Not. 51(9), 476-489 (2016) · Zbl 1361.68037 |
| [9] | Galatos, N.; Jipsen, P.; Kowalski, T.; Ono, H., Residuated Lattices: An Algebraic Glimpse at Substructural Logics (2007), Amsterdam: Elsevier, Amsterdam · Zbl 1171.03001 |
| [10] | Gehrke, M.; Priestley, H., Canonical extensions of double quasioperator algebras: an algebraic perspective on duality for certain algebras with binary operations, J. Pure Appl. Algebra, 209, 1, 269-290 (2007) · Zbl 1110.06015 · doi:10.1016/j.jpaa.2006.06.001 |
| [11] | Gehrke, M.; Priestley, H., Duality for double quasioperator algebras via their canonical extensions, Stud. Logica., 86, 1, 31-68 (2007) · Zbl 1127.06009 · doi:10.1007/s11225-007-9045-x |
| [12] | Ghica, DR; Smith, AI; Shao, Z., Bounded linear types in a resource semiring, Programming Languages and Systems, 331-350 (2014), Heidelberg: Springer, Heidelberg · Zbl 1405.68059 · doi:10.1007/978-3-642-54833-8_18 |
| [13] | van Gool, S., Guatto, A., Metcalfe, G., Santschi, S.: Time warps, from algebra to algorithms (with appendix) (2021). https://arxiv.org/abs/2106.06205 |
| [14] | Guatto, A.: A generalized modality for recursion. In: Dawar, A., Grädel, E. (eds.) Proceedings of LICS 2018, pp. 482-491. ACM (2018) · Zbl 1497.68093 |
| [15] | Holland, W.; McCleary, S., Solvability of the word problem in free lattice-ordered groups, Houston J. Math., 5, 1, 99-105 (1979) · Zbl 0387.06011 |
| [16] | Howard, W.A.: The formulae-as-types notion of construction. In: Curry, H., Hindley, B., Roger, S.J., Jonathan, P. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp. 479-490. Academic Press (1980) |
| [17] | Läuchli, H.; Leonard, J., On the elementary theory of linear order, Fund. Math., 59, 109-116 (1966) · Zbl 0156.25301 · doi:10.4064/fm-59-1-109-116 |
| [18] | Leroy, X., Doligez, D., Frisch, A., Garrigue, J., Rémy, D., Vouillon, J.: The OCaml system release 4.12 (2021). https://ocaml.org/releases/4.12/htmlman/index.html |
| [19] | Lucassen, J., Gifford, D.: Polymorphic effect systems. In: Proceedings of POPL 1988, pp. 47-57. ACM (1988) |
| [20] | Metcalfe, G., Paoli, F., Tsinakis, C.: Ordered algebras and logic. In: Hosni, H., Montagna, F. (eds.) Uncertainty and Rationality, vol. 10, pp. 1-85. Publications of the Scuola Normale Superiore di Pisa (2010) |
| [21] | de Moura, L.; Bjørner, N.; Ramakrishnan, CR; Rehof, J., Z3: an efficient SMT solver, Tools and Algorithms for the Construction and Analysis of Systems, 337-340 (2008), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-540-78800-3_24 |
| [22] | Nakano, H.: A modality for recursion. In: Proceedings of LICS 2000, pp. 255-266. IEEE (2000) |
| [23] | Santocanale, L.; Fahrenberg, U.; Jipsen, P.; Winter, M., The involutive quantaloid of completely distributive lattices, Relational and Algebraic Methods in Computer Science, 286-301 (2020), Cham: Springer, Cham · Zbl 07578348 · doi:10.1007/978-3-030-43520-2_18 |
| [24] | The Agda Development Team: The Agda Dependently-Typed Programming Language (2021). https://wiki.portal.chalmers.se/agda/Main/HomePage |
| [25] | The Coq Development Team: The Coq Proof Assistant (2021). https://coq.inria.fr |
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.
