{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:24:31Z","timestamp":1759638271328,"version":"3.37.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319893655"},{"type":"electronic","value":"9783319893662"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89366-2_17","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T19:52:34Z","timestamp":1523649154000},"page":"313-330","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Guarded Traced Categories"],"prefix":"10.1007","author":[{"given":"Sergey","family":"Goncharov","sequence":"first","affiliation":[]},{"given":"Lutz","family":"Schr\u00f6der","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Abel, A., Pientka, B.: Wellfounded recursion with copatterns: a unified approach to termination and productivity. In: International Conference on Functional Programming, ICFP 2013, pp. 185\u2013196. ACM (2013)","DOI":"10.1145\/2500365.2500591"},{"key":"17_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0022-4049(98)00106-6","volume":"143","author":"S Abramsky","year":"1999","unstructured":"Abramsky, S., Blute, R., Panangaden, P.: Nuclear and trace ideals in tensored*-categories. J. Pure Appl. Algebra 143, 3\u201347 (1999)","journal-title":"J. Pure Appl. Algebra"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Coecke, B.: A categorical semantics of quantum protocols. In: Logic in Computer Science, LICS 2004, pp. 415\u2013425. IEEE Computer Society (2004)","DOI":"10.1109\/LICS.2004.1319636"},{"issue":"5","key":"17_CR4","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1017\/S0960129502003730","volume":"12","author":"S Abramsky","year":"2002","unstructured":"Abramsky, S., Haghverdi, E., Scott, P.: Geometry of interaction and linear combinatory algebras. Math. Struct. Comput. Sci. 12(5), 625\u2013665 (2002)","journal-title":"Math. Struct. Comput. Sci."},{"key":"17_CR5","doi-asserted-by":"publisher","first-page":"7:1","DOI":"10.1145\/1614431.1614438","volume":"11","author":"R Arthan","year":"2009","unstructured":"Arthan, R., Martin, U., Mathiesen, E., Oliva, P.: A general framework for sound and complete Floyd-Hoare logics. ACM Trans. Comput. Log. 11, 7:1\u20137:31 (2009)","journal-title":"ACM Trans. Comput. Log."},{"key":"17_CR6","volume-title":"Process Algebra: Equational Theories of Communicating Processes","author":"J Baeten","year":"2010","unstructured":"Baeten, J., Basten, T., Reniers, M.: Process Algebra: Equational Theories of Communicating Processes. Cambridge University Press, Cambridge (2010)"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Birkedal, L., M\u00f8gelberg, R., 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:1), 1\u201345 (2012)","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"17_CR8","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/S0022-4049(99)00180-2","volume":"154","author":"R Blute","year":"2000","unstructured":"Blute, R., Cockett, R., Seely, R.: Feedback for linearly distributive categories: traces and fixpoints. J. Pure Appl. Algebra 154, 27\u201369 (2000)","journal-title":"J. Pure Appl. Algebra"},{"issue":"2","key":"17_CR9","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BF01705890","volume":"4","author":"R Book","year":"1970","unstructured":"Book, R., Greibach, S.: Quasi-realtime languages. Math. Syst. Theory 4(2), 97\u2013111 (1970)","journal-title":"Math. Syst. Theory"},{"key":"17_CR10","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/S0304-3975(01)00243-2","volume":"294","author":"A Bucalo","year":"2003","unstructured":"Bucalo, A., F\u00fchrmann, C., Simpson, A.: An equational notion of lifting monad. Theoret. Comput. Sci. 294, 31\u201360 (2003)","journal-title":"Theoret. Comput. Sci."},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Crole, R., Pitts, A.: New foundations for fixpoint computations. In: Logic in Computer Science, LICS 1990, pp. 489\u2013497. IEEE Computer Society (1990)","DOI":"10.1109\/LICS.1990.113771"},{"issue":"1","key":"17_CR12","first-page":"65","volume":"14","author":"Z \u00c9sik","year":"1999","unstructured":"\u00c9sik, Z.: Axiomatizing iteration categories. Acta Cybern. 14(1), 65\u201382 (1999)","journal-title":"Acta Cybern."},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-662-48057-1_2","volume-title":"Mathematical Foundations of Computer Science 2015","author":"Z \u00c9sik","year":"2015","unstructured":"\u00c9sik, Z.: Equational properties of fixed point operations in Cartesian categories: an overview. In: Italiano, G.F., Pighizzini, G., Sannella, D.T. (eds.) MFCS 2015. LNCS, vol. 9234, pp. 18\u201337. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48057-1_2"},{"issue":"69\u2013108","key":"17_CR14","first-page":"6","volume":"92","author":"J-Y Girard","year":"1989","unstructured":"Girard, J.-Y.: Towards a geometry of interaction. Contemp. Math. 92(69\u2013108), 6 (1989)","journal-title":"Contemp. Math."},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Goncharov, S., Schr\u00f6der, L.: A relatively complete generic Hoare logic for order-enriched effects. In: Proceedings of 28th Annual Symposium on Logic in Computer Science (LICS 2013), pp. 273\u2013282. IEEE (2013)","DOI":"10.1109\/LICS.2013.33"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/978-3-662-54458-7_30","volume-title":"Foundations of Software Science and Computation Structures","author":"S Goncharov","year":"2017","unstructured":"Goncharov, S., Schr\u00f6der, L., Rauch, C., Pir\u00f3g, M.: Unifying guarded and unguarded iteration. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 517\u2013533. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54458-7_30"},{"key":"17_CR17","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1017\/S096012951000006X","volume":"20","author":"E Haghverdi","year":"2010","unstructured":"Haghverdi, E., Scott, P.: Towards a typed geometry of interaction. Math. Struct. Comput. Sci. 20, 473\u2013521 (2010)","journal-title":"Math. Struct. Comput. Sci."},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/3-540-62688-3_37","volume-title":"Typed Lambda Calculi and Applications","author":"M Hasegawa","year":"1997","unstructured":"Hasegawa, M.: Recursion from cyclic sharing: traced monoidal categories and models of cyclic lambda calculi. In: de Groote, P., Roger Hindley, J. (eds.) TLCA 1997. LNCS, vol. 1210, pp. 196\u2013213. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-62688-3_37"},{"key":"17_CR19","series-title":"Distinguished Dissertations","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0865-8","volume-title":"Models of Sharing Graphs: A Categorical Semantics of let and letrec","author":"M Hasegawa","year":"1999","unstructured":"Hasegawa, M.: Models of Sharing Graphs: A Categorical Semantics of let and letrec. Distinguished Dissertations. Springer, London (1999). https:\/\/doi.org\/10.1007\/978-1-4471-0865-8"},{"key":"17_CR20","unstructured":"Jeffrey, A.: Premonoidal categories and flow graphs. In: Higher-Order Operational Techniques in Semantics, HOOTS 1997, vol. 10 of ENTCS, p. 51. Elsevier (1997)"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Jeffrey, A.: LTL types FRP: linear-time temporal logic propositions as types, proofs as functional reactive programs. In: Programming Languages Meets Program Verification, PLPV 2012, pp. 49\u201360. ACM (2012)","DOI":"10.1145\/2103776.2103783"},{"key":"17_CR22","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1017\/S0305004100074338","volume":"119","author":"A Joyal","year":"1996","unstructured":"Joyal, A., Street, R., Verity, D.: Traced monoidal categories. Math. Proc. Camb. Philos. Soc. 119, 447\u2013468 (1996)","journal-title":"Math. Proc. Camb. Philos. Soc."},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Kadison, R., Ringrose, J.: Fundamentals of the Theory of Operator Algebras: Advanced Theory, vol. 2. AMS (1997)","DOI":"10.1090\/gsm\/015"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Krishnaswami, N., Benton, N.: Ultrametric semantics of reactive programs. In: Logic in Computer Science, LICS 2011, pp. 257\u2013266. IEEE Computer Society (2011)","DOI":"10.1109\/LICS.2011.38"},{"key":"17_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-9839-7","volume-title":"Categories for the Working Mathematician","author":"S MacLane","year":"1971","unstructured":"MacLane, S.: Categories for the Working Mathematician. Springer, New York (1971). https:\/\/doi.org\/10.1007\/978-1-4612-9839-7"},{"key":"17_CR26","doi-asserted-by":"publisher","first-page":"2563","DOI":"10.1016\/j.jpaa.2012.03.026","volume":"216","author":"O Malherbe","year":"2012","unstructured":"Malherbe, O., Scott, P.J., Selinger, P.: Partially traced categories. J. Pure Appl. Algebra 216, 2563\u20132585 (2012)","journal-title":"J. Pure Appl. Algebra"},{"key":"17_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ic.2004.05.003","volume":"196","author":"S Milius","year":"2005","unstructured":"Milius, S.: Completely iterative algebras and completely iterative monads. Inf. Comput. 196, 1\u201341 (2005)","journal-title":"Inf. Comput."},{"key":"17_CR28","first-page":"407","volume":"150","author":"S Milius","year":"2017","unstructured":"Milius, S., Litak, T.: Guard your daggers and traces: properties of guarded (co-)recursion. Fund. Inf. 150, 407\u2013449 (2017)","journal-title":"Fund. Inf."},{"key":"17_CR29","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall Inc., Upper Saddle River (1989)"},{"key":"17_CR30","doi-asserted-by":"crossref","unstructured":"M\u00f8gelberg, R.: A type theory for productive coprogramming via guarded recursion. In: Computer Science Logic\/Logic in Computer Science, CSL-LICS 2014, pp. 71:1\u201371:10. ACM (2014)","DOI":"10.1145\/2603088.2603132"},{"key":"17_CR31","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Inf. Comput. 93, 55\u201392 (1991)","journal-title":"Inf. Comput."},{"key":"17_CR32","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/j.entcs.2014.10.015","volume":"308","author":"Maciej Pir\u00f3g","year":"2014","unstructured":"Pir\u00f3g, M., Gibbons, J.: The coinductive resumption monad. In: Mathematical Foundations of Programming Semantics, MFPS 2014. ENTCS, vol. 308, pp. 273\u2013288 (2014)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"17_CR33","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(00)00056-6","volume":"249","author":"J Rutten","year":"2000","unstructured":"Rutten, J.: Universal coalgebra: a theory of systems. Theoret. Comput. Sci. 249, 3\u201380 (2000)","journal-title":"Theoret. Comput. Sci."},{"key":"17_CR34","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1017\/S0960129504004256","volume":"14","author":"P Selinger","year":"2004","unstructured":"Selinger, P.: Towards a quantum programming language. Math. Struct. Comput. Sci. 14, 527\u2013586 (2004)","journal-title":"Math. Struct. Comput. Sci."},{"key":"17_CR35","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/j.entcs.2006.12.018","volume":"170","author":"Peter Selinger","year":"2007","unstructured":"Selinger, P.: Dagger compact closed categories and completely positive maps. In: Quantum Programming Languages, QPL 2005. ENTCS, vol. 170, pp. 139\u2013163. Elsevier (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"17_CR36","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-642-12821-9_4","volume-title":"New Structures for Physics. Lecture Notes in Physics","author":"P Selinger","year":"2010","unstructured":"Selinger, P.: A survey of graphical languages for monoidal categories. In: Coecke, B. (ed.) New Structures for Physics. Lecture Notes in Physics, vol. 813, pp. 289\u2013355. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12821-9_4"},{"key":"17_CR37","unstructured":"Simpson, A.: Recursive types in Kleisli categories. Technical report, University of Edinburgh (1992)"},{"key":"17_CR38","doi-asserted-by":"crossref","unstructured":"Simpson, A., Plotkin, G.: Complete axioms for categorical fixed-point operators. In: Logic in Computer Science, LICS 2000, pp. 30\u201341 (2000)","DOI":"10.1109\/LICS.2000.855753"},{"key":"17_CR39","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages","author":"G Winskel","year":"1993","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89366-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,15]],"date-time":"2019-10-15T16:22:07Z","timestamp":1571156527000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89366-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319893655","9783319893662"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89366-2_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}