{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,22]],"date-time":"2026-07-22T11:41:00Z","timestamp":1784720460375,"version":"3.55.0"},"reference-count":49,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2017,4,18]],"date-time":"2017-04-18T00:00:00Z","timestamp":1492473600000},"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":[[2018,4]]},"abstract":"<jats:p>Coinductive predicates express persisting \u2018safety\u2019 specifications of transition systems. Previous observations by Hermida and Jacobs identify coinductive predicates as suitable final coalgebras in a<jats:italic>fibration<\/jats:italic>\u2013 a categorical abstraction of predicate logic. In this paper, we follow the spirit of a seminal work by Worrell and study final sequences in a fibration. Our main contribution is to identify some categorical \u2018size restriction\u2019 axioms that guarantee stabilization of final sequences after \u03c9 steps. In its course, we develop a relevant categorical infrastructure that relates fibrations and locally presentable categories, a combination that does not seem to be studied a lot. The genericity of our fibrational framework can be exploited for binary relations (i.e. the logic of \u2018binary predicates\u2019) for which a coinductive predicate is bisimilarity, constructive logics (where interests are growing in coinductive predicates) and logics for name-passing processes.<\/jats:p>","DOI":"10.1017\/s0960129517000056","type":"journal-article","created":{"date-parts":[[2017,4,18]],"date-time":"2017-04-18T06:26:40Z","timestamp":1492496800000},"page":"562-611","source":"Crossref","is-referenced-by-count":10,"title":["Coinductive predicates and final sequences in a fibration"],"prefix":"10.1017","volume":"28","author":[{"given":"ICHIRO","family":"HASUO","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"TOSHIKI","family":"KATAOKA","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"KENTA","family":"CHO","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2017,4,18]]},"reference":[{"key":"S0960129517000056_ref49","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.12.009"},{"key":"S0960129517000056_ref48","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.06.003"},{"key":"S0960129517000056_ref43","unstructured":"Pattinson D. (2003). An introduction to the theory of coalgebras. Course notes for NASSLLI. Available online."},{"key":"S0960129517000056_ref37","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-5(3:10)2009"},{"key":"S0960129517000056_ref36","first-page":"177","volume-title":"MFPS XXIII","author":"Klin","year":"2007"},{"key":"S0960129517000056_ref35","unstructured":"Jacobs B. (2012). Introduction to coalgebra. Towards mathematics of states and observations. Draft of a book (ver. 2.0), available online."},{"key":"S0960129517000056_ref33","volume-title":"Coalgebraic Methods in Computer Science","author":"Jacobs","year":"2004"},{"key":"S0960129517000056_ref30","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2725"},{"key":"S0960129517000056_ref29","doi-asserted-by":"crossref","unstructured":"Hermida C. (1993). Fibrations, Logical Predicates and Indeterminates. PhD thesis, Univ. Edinburgh. Techn. rep. LFCS-93-277.","DOI":"10.7146\/dpb.v22i462.6935"},{"key":"S0960129517000056_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0026991"},{"key":"S0960129517000056_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"S0960129517000056_ref26","doi-asserted-by":"crossref","first-page":"718","DOI":"10.1145\/2837614.2837673","volume-title":"Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Hasuo","year":"2016"},{"key":"S0960129517000056_ref25","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-3(4:11)2007"},{"key":"S0960129517000056_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_31"},{"key":"S0960129517000056_ref41","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.10.017"},{"key":"S0960129517000056_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0059396"},{"key":"S0960129517000056_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.12.005"},{"key":"S0960129517000056_ref32","volume-title":"Categorical Logic and Type Theory","author":"Jacobs","year":"1999"},{"key":"S0960129517000056_ref19","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.08.004"},{"key":"S0960129517000056_ref18","first-page":"93","volume-title":"Logic in Computer Science","author":"Fiore","year":"2001"},{"key":"S0960129517000056_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.09.021"},{"key":"S0960129517000056_ref16","first-page":"129","volume-title":"Foundations of Software Science and Computation Structures, Proceedings of the 5th International Conference, FoSSaCS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software","author":"Ferrari","year":"2002"},{"key":"S0960129517000056_ref15","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1979.82.43"},{"key":"S0960129517000056_ref12","first-page":"179","volume-title":"CSL","author":"C\u00eerstea","year":"2009"},{"key":"S0960129517000056_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.04.025"},{"key":"S0960129517000056_ref42","first-page":"353","volume-title":"APLAS","author":"Nakata","year":"2011"},{"key":"S0960129517000056_ref10","volume-title":"Handbook of Modal Logic","author":"Bradfield","year":"2006"},{"key":"S0960129517000056_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429124"},{"key":"S0960129517000056_ref34","unstructured":"Jacobs B. (2010). Predicate logic for functors and monads. Preprint, available at the author's webpage."},{"key":"S0960129517000056_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.05.020"},{"key":"S0960129517000056_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00240-7"},{"key":"S0960129517000056_ref39","volume-title":"Sheaves in Geometry and Logic. A First Introduction to Topos Theory","author":"MacAAAALane","year":"1992"},{"key":"S0960129517000056_ref24","first-page":"197","volume-title":"Mathematical Foundations of Programming Semantics (MFPS XXIX)","author":"Hasuo","year":"2013"},{"key":"S0960129517000056_ref3","first-page":"58","volume-title":"Proceedings of the Foundations of Software Science and Computational Structures - 15th International Conference, FoSSaCS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software","author":"Ad\u00e1mek","year":"2012"},{"key":"S0960129517000056_ref46","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561301"},{"key":"S0960129517000056_ref13","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxp004"},{"key":"S0960129517000056_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511600579"},{"key":"S0960129517000056_ref1","unstructured":"Abramsky S. and Winschel V. (2015). Coalgebraic analysis of subgame-perfect equilibria in infinite games without discounting. Mathematical Structures in Computer Science. To appear."},{"key":"S0960129517000056_ref38","first-page":"257","volume-title":"TbiLLC","author":"Kupke","year":"2007"},{"key":"S0960129517000056_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22944-2_13"},{"key":"S0960129517000056_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.05.018"},{"key":"S0960129517000056_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429093"},{"key":"S0960129517000056_ref8","first-page":"20","volume-title":"Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14","author":"Bonchi","year":"2014"},{"key":"S0960129517000056_ref44","doi-asserted-by":"publisher","DOI":"10.1007\/s00012-011-0129-0"},{"key":"S0960129517000056_ref6","first-page":"A831","article-title":"Th\u00e9ories relatives \u00e0 un corpus","volume":"281","author":"B\u00e9nabou","year":"1975","journal-title":"Comptes Rendus de l'Acad\u00e9mie des Sciences Paris"},{"key":"S0960129517000056_ref47","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(1:13)2011"},{"key":"S0960129517000056_ref45","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"S0960129517000056_ref5","first-page":"42","volume-title":"Proceedings of the Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software","author":"Atkey","year":"2012"},{"key":"S0960129517000056_ref40","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/104"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129517000056","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,27]],"date-time":"2022-07-27T15:31:59Z","timestamp":1658935919000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129517000056\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,4,18]]},"references-count":49,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,4]]}},"alternative-id":["S0960129517000056"],"URL":"https:\/\/doi.org\/10.1017\/s0960129517000056","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,4,18]]}}}