{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,2]],"date-time":"2026-04-02T01:00:04Z","timestamp":1775091604090,"version":"3.50.1"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030887001","type":"print"},{"value":"9783030887018","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-88701-8_19","type":"book-chapter","created":{"date-parts":[[2021,10,21]],"date-time":"2021-10-21T23:06:25Z","timestamp":1634857585000},"page":"309-324","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Time Warps, from Algebra to Algorithms"],"prefix":"10.1007","author":[{"given":"Sam","family":"van Gool","sequence":"first","affiliation":[]},{"given":"Adrien","family":"Guatto","sequence":"additional","affiliation":[]},{"given":"George","family":"Metcalfe","sequence":"additional","affiliation":[]},{"given":"Simon","family":"Santschi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,10,22]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Backus, J.W., et al.: The FORTRAN automatic coding system. In: Astrahan, M.M. (ed.) Proceedings of IRE-AIEE-ACM 1957 (Western), pp. 188\u2013198. ACM (1957)","DOI":"10.1145\/1455567.1455599"},{"issue":"4","key":"19_CR2","doi-asserted-by":"publisher","first-page":"55","DOI":"10.2168\/LMCS-8(4:1)2012","volume":"8","author":"L Birkedal","year":"2012","unstructured":"Birkedal, L., M\u00f8gelberg, R.E., Schwinghammer, J., St\u00f8vring, K.: First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Log. Methods Comput. Sci. 8(4), 55\u201364 (2012)","journal-title":"Log. Methods Comput. Sci."},{"issue":"4","key":"19_CR3","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1142\/S0218196703001511","volume":"13","author":"K Blount","year":"2003","unstructured":"Blount, K., Tsinakis, C.: The structure of residuated lattices. Int. J. Algebr. Comput. 13(4), 437\u2013461 (2003)","journal-title":"Int. J. Algebr. Comput."},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427\u2013442. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11609773_28"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Caspi, P., Pouzet, M.: Synchronous Kahn networks. In: Proceedings of ICFP 1996, pp. 226\u2013238. ACM (1996)","DOI":"10.1145\/232629.232651"},{"key":"19_CR6","unstructured":"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"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/978-3-662-49630-5_30","volume-title":"Foundations of Software Science and Computation Structures","author":"S Fujii","year":"2016","unstructured":"Fujii, S., Katsumata, S., Melli\u00e8s, P.-A.: Towards a formal theory of graded monads. In: Jacobs, B., L\u00f6ding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 513\u2013530. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49630-5_30"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Gaboardi, M., Katsumata, S.Y., Orchard, D., Breuvart, F., Uustalu, T.: Combining effects and coeffects via grading. ACM SIGPLAN Not. 51(9), 476\u2013489 (2016)","DOI":"10.1145\/3022670.2951939"},{"key":"19_CR9","volume-title":"Residuated Lattices: An Algebraic Glimpse at Substructural Logics","author":"N Galatos","year":"2007","unstructured":"Galatos, N., Jipsen, P., Kowalski, T., Ono, H.: Residuated Lattices: An Algebraic Glimpse at Substructural Logics. Elsevier, Amsterdam (2007)"},{"issue":"1","key":"19_CR10","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/j.jpaa.2006.06.001","volume":"209","author":"M Gehrke","year":"2007","unstructured":"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\u2013290 (2007)","journal-title":"J. Pure Appl. Algebra"},{"issue":"1","key":"19_CR11","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s11225-007-9045-x","volume":"86","author":"M Gehrke","year":"2007","unstructured":"Gehrke, M., Priestley, H.: Duality for double quasioperator algebras via their canonical extensions. Stud. Logica. 86(1), 31\u201368 (2007)","journal-title":"Stud. Logica."},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-642-54833-8_18","volume-title":"Programming Languages and Systems","author":"DR Ghica","year":"2014","unstructured":"Ghica, D.R., Smith, A.I.: Bounded linear types in a resource semiring. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 331\u2013350. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_18"},{"key":"19_CR13","unstructured":"van Gool, S., Guatto, A., Metcalfe, G., Santschi, S.: Time warps, from algebra to algorithms (with appendix) (2021). https:\/\/arxiv.org\/abs\/2106.06205"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Guatto, A.: A generalized modality for recursion. In: Dawar, A., Gr\u00e4del, E. (eds.) Proceedings of LICS 2018, pp. 482\u2013491. ACM (2018)","DOI":"10.1145\/3209108.3209148"},{"issue":"1","key":"19_CR15","first-page":"99","volume":"5","author":"W Holland","year":"1979","unstructured":"Holland, W., McCleary, S.: Solvability of the word problem in free lattice-ordered groups. Houston J. Math. 5(1), 99\u2013105 (1979)","journal-title":"Houston J. Math."},{"key":"19_CR16","unstructured":"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\u2013490. Academic Press (1980)"},{"key":"19_CR17","doi-asserted-by":"publisher","first-page":"109","DOI":"10.4064\/fm-59-1-109-116","volume":"59","author":"H L\u00e4uchli","year":"1966","unstructured":"L\u00e4uchli, H., Leonard, J.: On the elementary theory of linear order. Fund. Math. 59, 109\u2013116 (1966)","journal-title":"Fund. Math."},{"key":"19_CR18","unstructured":"Leroy, X., Doligez, D., Frisch, A., Garrigue, J., R\u00e9my, D., Vouillon, J.: The OCaml system release 4.12 (2021). https:\/\/ocaml.org\/releases\/4.12\/htmlman\/index.html"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Lucassen, J., Gifford, D.: Polymorphic effect systems. In: Proceedings of POPL 1988, pp. 47\u201357. ACM (1988)","DOI":"10.1145\/73560.73564"},{"key":"19_CR20","unstructured":"Metcalfe, G., Paoli, F., Tsinakis, C.: Ordered algebras and logic. In: Hosni, H., Montagna, F. (eds.) Uncertainty and Rationality, vol. 10, pp. 1\u201385. Publications of the Scuola Normale Superiore di Pisa (2010)"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"19_CR22","unstructured":"Nakano, H.: A modality for recursion. In: Proceedings of LICS 2000, pp. 255\u2013266. IEEE (2000)"},{"key":"19_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-030-43520-2_18","volume-title":"Relational and Algebraic Methods in Computer Science","author":"L Santocanale","year":"2020","unstructured":"Santocanale, L.: The involutive quantaloid of completely distributive lattices. In: Fahrenberg, U., Jipsen, P., Winter, M. (eds.) RAMiCS 2020. LNCS, vol. 12062, pp. 286\u2013301. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-43520-2_18"},{"key":"19_CR24","unstructured":"The Agda Development Team: The Agda Dependently-Typed Programming Language (2021). https:\/\/wiki.portal.chalmers.se\/agda\/Main\/HomePage"},{"key":"19_CR25","unstructured":"The Coq Development Team: The Coq Proof Assistant (2021). https:\/\/coq.inria.fr"}],"container-title":["Lecture Notes in Computer Science","Relational and Algebraic Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-88701-8_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,22]],"date-time":"2021-10-22T00:51:14Z","timestamp":1634863874000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-88701-8_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030887001","9783030887018"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-88701-8_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"22 October 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RAMiCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Relational and Algebraic Methods in Computer Science","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Marseille","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 November 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 November 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ramics2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ramics19.lis-lab.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}