{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T23:10:21Z","timestamp":1773097821459,"version":"3.50.1"},"reference-count":26,"publisher":"Cambridge University Press (CUP)","issue":"7","license":[{"start":{"date-parts":[[2016,2,9]],"date-time":"2016-02-09T00:00:00Z","timestamp":1454976000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2017,10]]},"abstract":"<jats:p>Induction is a well-established proof principle that is taught in most undergraduate programs in mathematics and computer science. In computer science, it is used primarily to reason about inductively defined datatypes such as finite lists, finite trees and the natural numbers. Coinduction is the dual principle that can be used to reason about coinductive datatypes such as infinite streams or trees, but it is not as widespread or as well understood. In this paper, we illustrate through several examples the use of coinduction in informal mathematical arguments. Our aim is to promote the principle as a useful tool for the working mathematician and to bring it to a level of familiarity on par with induction. We show that coinduction is not only about bisimilarity and equality of behaviors, but also applicable to a variety of functions and relations defined on coinductive datatypes.<\/jats:p>","DOI":"10.1017\/s0960129515000493","type":"journal-article","created":{"date-parts":[[2016,2,9]],"date-time":"2016-02-09T10:53:20Z","timestamp":1455015200000},"page":"1132-1152","source":"Crossref","is-referenced-by-count":25,"title":["Practical coinduction"],"prefix":"10.1017","volume":"27","author":[{"given":"DEXTER","family":"KOZEN","sequence":"first","affiliation":[]},{"given":"ALEXANDRA","family":"SILVA","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2016,2,9]]},"reference":[{"key":"S0960129515000493_ref10","first-page":"336","volume-title":"LICS","author":"Klin","year":"2007"},{"key":"S0960129515000493_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.09.023"},{"key":"S0960129515000493_ref1","unstructured":"Aczel P. (1988). Non-Well-Founded Sets, Number 14 in CSLI Lecture Notes, Center for the Study of Language and Information, Stanford, CA."},{"key":"S0960129515000493_ref19","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/7.2.175"},{"key":"S0960129515000493_ref26","doi-asserted-by":"crossref","unstructured":"Turi D. and Plotkin G.D. (1997). Towards a mathematical operational semantics. In: LICS 280\u2013291.","DOI":"10.1109\/LICS.1997.614955"},{"key":"S0960129515000493_ref21","first-page":"127","volume-title":"Lecture Notes in Computer Science","author":"Ro\u015fu","year":"2009"},{"key":"S0960129515000493_ref4","doi-asserted-by":"crossref","first-page":"309","DOI":"10.3233\/FI-1998-33401","article-title":"Coinductive axiomatization of recursive type equality and subtyping","volume":"33","author":"Brandt","year":"1998","journal-title":"Fundamenta Informaticae"},{"key":"S0960129515000493_ref5","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"Harel","year":"2000"},{"key":"S0960129515000493_ref7","first-page":"1","article-title":"Generic trace semantics via coinduction","volume":"3","author":"Ichiro","year":"2007","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129515000493_ref3","unstructured":"Barwise J. and Moss L. (1996). Vicious Circles: On the Mathematics of Non-Wellfounded Phenomena, Number 60 in CSLI Lecture Notes, Center for the Study of Language and Information, Stanford, CA."},{"key":"S0960129515000493_ref18","unstructured":"Niqui M. and Rutten J. (2009). Coinductive predicates as final coalgebras. In: Proceedings of the 6th Workshop on Fixed Points in Computer Science (FICS 2009) 79\u201385."},{"key":"S0960129515000493_ref16","unstructured":"Mendler N.P. (1988). Inductive Definition in Type Theory. PhD thesis, Cornell University."},{"key":"S0960129515000493_ref9","first-page":"185","article-title":"Computing with capsules","volume":"17","author":"Jeannin","year":"2012","journal-title":"J. Automata, Languages and Combinatorics"},{"key":"S0960129515000493_ref8","first-page":"493","volume-title":"Lecture Notes in Computer Science","author":"Jaffar","year":"2008"},{"key":"S0960129515000493_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31982-5_28"},{"key":"S0960129515000493_ref13","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-5(3:10)2009"},{"key":"S0960129515000493_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"S0960129515000493_ref12","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000657"},{"key":"S0960129515000493_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90033-X"},{"key":"S0960129515000493_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/BF01110627"},{"key":"S0960129515000493_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00125-0"},{"key":"S0960129515000493_ref6","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2725"},{"key":"S0960129515000493_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70918-3_49"},{"key":"S0960129515000493_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"S0960129515000493_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155231"},{"key":"S0960129515000493_ref20","volume-title":"Advanced Topics in Bisimulation and Coinduction","author":"Pous","year":"2011"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129515000493","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,15]],"date-time":"2020-09-15T04:41:30Z","timestamp":1600144890000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129515000493\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,2,9]]},"references-count":26,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2017,10]]}},"alternative-id":["S0960129515000493"],"URL":"https:\/\/doi.org\/10.1017\/s0960129515000493","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,2,9]]}}}