{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,22]],"date-time":"2026-07-22T11:41:07Z","timestamp":1784720467081,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":45,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662544570","type":"print"},{"value":"9783662544587","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-662-54458-7_7","type":"book-chapter","created":{"date-parts":[[2017,3,15]],"date-time":"2017-03-15T09:22:57Z","timestamp":1489569777000},"page":"106-123","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Companions, Codensity and Causality"],"prefix":"10.1007","author":[{"given":"Damien","family":"Pous","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jurriaan","family":"Rot","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,3,16]]},"reference":[{"issue":"4","key":"7_CR1","first-page":"267","volume":"5","author":"M Abadi","year":"1998","unstructured":"Abadi, M., Gordon, A.D.: A bisimulation method for cryptographic protocols. Nord. J. Comput. 5(4), 267 (1998)","journal-title":"Nord. J. Comput."},{"key":"7_CR2","unstructured":"Abramsky, S.: The lazy lambda calculus. In: Research Topics in Functional Programming, pp. 65\u2013116. Addison Wesley (1990)"},{"issue":"4","key":"7_CR3","first-page":"589","volume":"15","author":"J Ad\u00e1mek","year":"1974","unstructured":"Ad\u00e1mek, J.: Free algebras and automata realizations in the language of categories. Commentationes Mathematicae Universitatis Carolinae 15(4), 589\u2013602 (1974)","journal-title":"Commentationes Mathematicae Universitatis Carolinae"},{"issue":"3","key":"7_CR4","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/0022-4049(92)90169-G","volume":"82","author":"M Barr","year":"1992","unstructured":"Barr, M.: Algebraically compact functors. J. Pure Appl. Algebra 82(3), 211\u2013231 (1992)","journal-title":"J. Pure Appl. Algebra"},{"key":"7_CR5","unstructured":"Bartels, F.: On generalised coinduction and probabilistic specification formats. PhD thesis, CWI, Amsterdam, April 2004"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Bonchi, F., Petrisan, D., Pous, D., Rot, J.: Coinduction up-to in a fibrational setting. In: Proceeding CSL-LICS, pp. 20:1\u201320:9. ACM (2014)","DOI":"10.1145\/2603088.2603149"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Bonchi, F., Petri\u015fan, D., Pous, D., Rot, J.: A general account of coinduction up-to. Acta Informatica, pp. 1\u201364 (2016)","DOI":"10.1007\/s00236-016-0271-4"},{"key":"7_CR8","series-title":"Mathematics and its Applications","volume-title":"Shape Theory: Categorical Methods of Approximation","author":"J-M Cordier","year":"1989","unstructured":"Cordier, J.-M., Porter, T.: Shape Theory: Categorical Methods of Approximation. Mathematics and its Applications. Ellis Horwood, New York (1989). Reprinted by Dover, 2008"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-39634-2_26","volume-title":"Interactive Theorem Proving","author":"J Endrullis","year":"2013","unstructured":"Endrullis, J., Hendriks, D., Bodin, M.: Circular coinduction in coq using bisimulation-up-to techniques. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 354\u2013369. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39634-2_26"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/3-540-44929-9_26","volume-title":"Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics","author":"C Fournet","year":"2000","unstructured":"Fournet, C., L\u00e9vy, J.-J., Schmitt, A.: An asynchronous, distributed implementation of mobile ambients. In: Leeuwen, J., Watanabe, O., Hagiya, M., Mosses, P.D., Ito, T. (eds.) TCS 2000. LNCS, vol. 1872, pp. 348\u2013364. Springer, Heidelberg (2000). doi:10.1007\/3-540-44929-9_26"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Gambino, N., Kock, J.: Polynomial functors and polynomial monads. In: Proceeding of Mathematical proceedings of the cambridge philosophical society, vol. 154, pp. 153\u2013192. Cambridge University Press (2013)","DOI":"10.1017\/S0305004112000394"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Hansen, H.H., Kupke, C., Rutten, J.: Stream differential equations: specification formats and solution methods. CoRR, abs\/1609.08367 (2016)","DOI":"10.23638\/LMCS-13(1:3)2017"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Hur, C., Neis, G., Dreyer, D., Vafeiadis, V.: The power of parameterization in coinductive proof. In: Proceeding of POPL, pp. 193\u2013206. ACM (2013)","DOI":"10.1145\/2480359.2429093"},{"issue":"4","key":"7_CR14","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1016\/j.ic.2005.03.006","volume":"204","author":"B Jacobs","year":"2006","unstructured":"Jacobs, B.: Distributive laws for the coinductive solution of recursive equations. Inf. Comput. 204(4), 561\u2013587 (2006)","journal-title":"Inf. Comput."},{"key":"7_CR15","unstructured":"Jacobs, B.: Introduction to coalgebra. Towards mathematics of states and observations. Draft (2014)"},{"issue":"1\u20133","key":"7_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2004.03.005","volume":"323","author":"A Jeffrey","year":"2004","unstructured":"Jeffrey, A., Rathke, J.: A theory of bisimulation for a fragment of concurrent ML with local names. Theor. Comput. Sci. 323(1\u20133), 1\u201348 (2004)","journal-title":"Theor. Comput. Sci."},{"issue":"38","key":"7_CR17","doi-asserted-by":"publisher","first-page":"5043","DOI":"10.1016\/j.tcs.2011.03.023","volume":"412","author":"B Klin","year":"2011","unstructured":"Klin, B.: Bialgebras for structural operational semantics: an introduction. Theor. Comput. Sci. 412(38), 5043\u20135069 (2011)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR18","unstructured":"Klin, B., Nachyla, B.: Presenting morphisms of distributive laws. In: Proceeding CALCO, vol. 35. LIPIcs, pp. 190\u2013204. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)"},{"key":"7_CR19","first-page":"133","volume":"6","author":"B Knaster","year":"1928","unstructured":"Knaster, B.: Un th\u00e9or\u00e8me sur les fonctions d\u2019ensembles. Annales de la Socit Polonaise de Mathmatiques 6, 133\u2013134 (1928)","journal-title":"Annales de la Socit Polonaise de Mathmatiques"},{"key":"7_CR20","volume-title":"Categories for the Working Mathematician","author":"SM Lane","year":"1998","unstructured":"Lane, S.M.: Categories for the Working Mathematician. Springer, New York (1998)"},{"issue":"13","key":"7_CR21","first-page":"332","volume":"28","author":"T Leinster","year":"2013","unstructured":"Leinster, T.: Codensity and the ultrafilter monad. Theory and Applications of Categories 28(13), 332\u2013370 (2013)","journal-title":"Theory and Applications of Categories"},{"key":"7_CR22","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1016\/S1571-0661(05)80350-0","volume":"33","author":"M Lenisa","year":"2000","unstructured":"Lenisa, M., Power, J., Watanabe, H.: Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads. Electron. Notes Theor. Comput. Sci. 33, 230\u2013260 (2000)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1\u20132","key":"7_CR23","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/j.tcs.2004.07.024","volume":"327","author":"M Lenisa","year":"2004","unstructured":"Lenisa, M., Power, J., Watanabe, H.: Category theory for operational semantics. Theor. Comput. Sci. 327(1\u20132), 135\u2013154 (2004)","journal-title":"Theor. Comput. Sci."},{"issue":"7","key":"7_CR24","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Milius, S., Moss, L.S., Schwencke, D.: Abstract GSOS rules and a modular treatment of recursive definitions. Logical Methods Comput. Sci. 9(3) (2013)","DOI":"10.2168\/LMCS-9(3:28)2013"},{"key":"7_CR26","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall (1989)"},{"issue":"1","key":"7_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes I\/II. Inf. Comput. 100(1), 1\u201377 (1992)","journal-title":"Inf. Comput."},{"key":"7_CR28","unstructured":"nLab article. Kan extension 2016. (Revision 103), http:\/\/ncatlab.org\/nlab\/show\/Kan+extension"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Parrow, J., Weber, T.: The largest respectful function. Logical Methods Comput. Sci. 12(2) (2016)","DOI":"10.2168\/LMCS-12(2:11)2016"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-540-76637-7_24","volume-title":"Programming Languages and Systems","author":"D Pous","year":"2007","unstructured":"Pous, D.: Complete lattices and up-to techniques. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 351\u2013366. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-76637-7_24"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"Pous,D.: Coinduction all the way up. In: Proceeding LICS, pp. 307-316. ACM (2016)","DOI":"10.1145\/2933575.2934564"},{"key":"7_CR32","unstructured":"Pous, D., Rot, J.: Companions, Codensity, and Causality. In: Esparza, J., Murawski, A.S. (eds.) FOSSACS 2017 LNCS, vol. 10203, pp. 106\u2013123. Springer, Heidelberg (2017). (version with proofs), https:\/\/hal.archives-ouvertes.fr\/hal-01442222"},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"Pous, D., Sangiorgi, D.: Advanced Topics in Bisimulation and Coinduction, chapter about \u201cEnhancements of the coinductive proof method\u201d. Cambridge University Press (2011)","DOI":"10.1017\/CBO9780511792588"},{"issue":"1\u20132","key":"7_CR34","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/S0304-3975(01)00024-X","volume":"280","author":"J Power","year":"2002","unstructured":"Power, J., Watanabe, H.: Combining a monad and a comonad. Theor. Comput. Sci. 280(1\u20132), 137\u2013162 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR35","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1016\/j.ic.2015.11.009","volume":"246","author":"J Rot","year":"2016","unstructured":"Rot, J., Bonsangue, M.M., Rutten, J.: Proving language inclusion and equivalence by coinduction. Inf. Comput. 246, 62\u201376 (2016)","journal-title":"Inf. Comput."},{"key":"7_CR36","unstructured":"Rot, J., Winter, J.: On language equations and grammar coalgebras for context-free languages. In: Proceeding CALCO Early Ideas (2013)"},{"issue":"1","key":"7_CR37","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1017\/S0960129504004517","volume":"15","author":"JJMM Rutten","year":"2005","unstructured":"Rutten, J.J.M.M.: A coinductive calculus of streams. Math. Struct. Comput. Sci. 15(1), 93\u2013147 (2005)","journal-title":"Math. Struct. Comput. Sci."},{"key":"7_CR38","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1017\/S0960129598002527","volume":"8","author":"D Sangiorgi","year":"1998","unstructured":"Sangiorgi, D.: On the bisimulation proof method. Math. Struct. Comput. Sci. 8, 447\u2013479 (1998)","journal-title":"Math. Struct. Comput. Sci."},{"key":"7_CR39","doi-asserted-by":"crossref","unstructured":"Sangiorgi, D., Walker, D.: The $$\\pi $$-calculus: a theory of mobile processes. Cambridge University Press (2001)","DOI":"10.1017\/9781316134924"},{"issue":"3","key":"7_CR40","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1145\/2487241.2487248","volume":"60","author":"J Sevc\u00edk","year":"2013","unstructured":"Sevc\u00edk, J., Vafeiadis, V., Nardelli, F.Z., Jagannathan, S., Sewell, P.: CompCertTSO: a verified compiler for relaxed-memory concurrency. J. ACM 60(3), 22 (2013)","journal-title":"J. ACM"},{"key":"7_CR41","unstructured":"Silva, A., Bonchi, F., Bonsangue, M., Rutten, J.: Generalizing the powerset construction, coalgebraically. In: Proceeding FSTTCS, pp. 272\u2013283 (2010)"},{"issue":"2","key":"7_CR42","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem, its applications. Pacific J. Math. 5(2), 285\u2013309 (1955)","journal-title":"Pacific J. Math."},{"key":"7_CR43","doi-asserted-by":"crossref","unstructured":"Turi, D., Plotkin, G.D.: Towards a mathematical operational semantics. In: Proceeding LICS, pp. 280-291. IEEE (1997)","DOI":"10.1109\/LICS.1997.614955"},{"issue":"1","key":"7_CR44","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/S1571-0661(04)80372-4","volume":"65","author":"H Watanabe","year":"2002","unstructured":"Watanabe, H.: Well-behaved translations between structural operational semantics. Electron. Notes Theor. Comput. Sci. 65(1), 337\u2013357 (2002)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"7_CR45","doi-asserted-by":"crossref","unstructured":"Winter, J., Bonsangue, M.M., Rutten, J.J.M.M.: Coalgebraic characterizations of context-free languages. Logical Methods Comput. Sci. 9(3) (2013)","DOI":"10.2168\/LMCS-9(3:14)2013"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54458-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T21:22:28Z","timestamp":1750108948000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54458-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662544570","9783662544587"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54458-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"16 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}