{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,2]],"date-time":"2026-04-02T02:29:47Z","timestamp":1775096987979,"version":"3.50.1"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"DFF","award":["4002-00442"],"award-info":[{"award-number":["4002-00442"]}]},{"DOI":"10.13039\/100008398","name":"VILLUM FONDEN","doi-asserted-by":"crossref","award":["13156"],"award-info":[{"award-number":["13156"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>In type theory, coinductive types are used to represent processes, and are thus crucial for the formal verification of non-terminating reactive programs in proof assistants based on type theory, such as Coq and Agda. Currently, programming and reasoning about coinductive types is difficult for two reasons: The need for recursive definitions to be productive, and the lack of coincidence of the built-in identity types and the important notion of bisimilarity.<\/jats:p>\n          <jats:p>Guarded recursion in the sense of Nakano has recently been suggested as a possible approach to dealing with the problem of productivity, allowing this to be encoded in types. Indeed, coinductive types can be encoded using a combination of guarded recursion and universal quantification over clocks. This paper studies the notion of bisimilarity for guarded recursive types in Ticked Cubical Type Theory, an extension of Cubical Type Theory with guarded recursion. We prove that, for any functor, an abstract, category theoretic notion of bisimilarity for the final guarded coalgebra is equivalent (in the sense of homotopy type theory) to path equality (the primitive notion of equality in cubical type theory). As a worked example we study a guarded notion of labelled transition systems, and show that, as a special case of the general theorem, path equality coincides with an adaptation of the usual notion of bisimulation for processes. In particular, this implies that guarded recursion can be used to give simple equational reasoning proofs of bisimilarity. This work should be seen as a step towards obtaining bisimilarity as path equality for coinductive types using the encodings mentioned above.<\/jats:p>","DOI":"10.1145\/3290317","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Bisimulation as path type for guarded recursive types"],"prefix":"10.1145","volume":"3","author":[{"given":"Rasmus Ejlers","family":"M\u00f8gelberg","sequence":"first","affiliation":[{"name":"IT University of Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Niccol\u00f2","family":"Veltri","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000319"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10485-014-9372-9"},{"key":"e_1_2_2_3_1","volume-title":"Non-Wellfounded Trees in Homotopy Type Theory. In 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015","volume":"38","author":"Ahrens Benedikt","year":"2015"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500597"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/3329995.3330032"},{"key":"e_1_2_2_7_1","volume-title":"19th International Conference on Types for Proofs and Programs, TYPES 2013","volume":"26","author":"Bezem Marc","year":"2013"},{"key":"e_1_2_2_8_1","volume-title":"Guarded Cubical Type Theory: Path Equality for Guarded Recursion. In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016","author":"Birkedal Lars","year":"2016"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.16"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08918-8_8"},{"key":"e_1_2_2_11_1","volume-title":"Ranald Clouston, Rasmus Ejlers M\u00f8gelberg, and Lars Birkedal.","author":"Bizjak Ales","year":"2016"},{"key":"e_1_2_2_12_1","volume-title":"Type-driven Development with Idris","author":"Brady Edwin"},{"key":"e_1_2_2_13_1","volume-title":"21st International Conference on Types for Proofs and Programs (TYPES 2015) (Leibniz International Proceedings in Informatics (LIPIcs))","author":"Cohen Cyril"},{"key":"e_1_2_2_14_1","volume-title":"International Workshop TYPES\u201993","volume":"806","author":"Coquand Thierry","year":"1993"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209197"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158131"},{"key":"e_1_2_2_17_1","volume-title":"International Workshop TYPES\u201995","volume":"1158","author":"Dybjer Peter","year":"1996"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167085"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/646234.758793"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2725"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"e_1_2_2_22_1","doi-asserted-by":"crossref","volume-title":"Introduction to Coalgebra: Towards Mathematics of States and Observation","author":"Jacobs Bart","DOI":"10.1017\/CBO9781316823187"},{"key":"e_1_2_2_23_1","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ale\u0161 Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris from the ground up. (2018). https:\/\/people.mpi- sws.org\/~dreyer\/papers\/iris- ground- up\/paper.pdf  Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ale\u0161 Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris from the ground up. (2018). https:\/\/people.mpi- sws.org\/~dreyer\/papers\/iris- ground- up\/paper.pdf"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.08.002"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_2_26_1","volume-title":"Sheaves in geometry and logic: A first introduction to topos theory","author":"MacLane Saunders"},{"key":"e_1_2_2_27_1","volume-title":"The Clocks They Are Adjunctions Denotational Semantics for Clocked Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018","volume":"108","author":"Mannaa Bassel","year":"2018"},{"key":"e_1_2_2_28_1","series-title":"Lecture Notes in Computer Science","volume-title":"A Calculus of Communicating Systems","author":"Milner Robin"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90114-7"},{"key":"e_1_2_2_30_1","volume-title":"Communicating and mobile systems: the pi calculus","author":"Milner Robin"},{"key":"e_1_2_2_31_1","first-page":"1","article-title":"A type theory for productive coprogramming via guarded recursion","volume":"71","author":"M\u00f8gelberg R. E.","year":"2014","journal-title":"CSL-LICS."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934516"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/788022.789002"},{"key":"e_1_2_2_34_1","volume-title":"25th EACSL Annual Conference on Computer Science Logic, CSL 2016","author":"Orton Ian","year":"2016"},{"key":"e_1_2_2_35_1","volume-title":"Advanced Topics in Bisimulation and Coinduction","author":"Pous Damien"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.10.010"},{"key":"e_1_2_2_38_1","unstructured":"Arnaud Spiwack and Thierry Coquand. 2010. Constructively Finite? In Contribuciones cient\u00edficas en honor de Mirian Andr\u00e9s G\u00f3mez Laureano Lamb\u00e1n Pardo Ana Romero Ib\u00e1\u00f1ez and Julio Rubio Garc\u00eda (Eds.). Universidad de La Rioja 217\u2013230.  Arnaud Spiwack and Thierry Coquand. 2010. Constructively Finite? In Contribuciones cient\u00edficas en honor de Mirian Andr\u00e9s G\u00f3mez Laureano Lamb\u00e1n Pardo Ana Romero Ib\u00e1\u00f1ez and Julio Rubio Garc\u00eda (Eds.). Universidad de La Rioja 217\u2013230."},{"key":"e_1_2_2_39_1","volume-title":"Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings (Lecture Notes in Computer Science), Alexander Kurz, Marina Lenisa, and Andrzej Tarlecki (Eds.)","volume":"5728","author":"Staton Sam","year":"2009"},{"key":"e_1_2_2_40_1","unstructured":"The Agda Team. 2018. The Agda wiki. (2018). http:\/\/wiki.portal.chalmers.se\/agda\/ .  The Agda Team. 2018. The Agda wiki. (2018). http:\/\/wiki.portal.chalmers.se\/agda\/ ."},{"key":"e_1_2_2_41_1","doi-asserted-by":"crossref","unstructured":"The Project Everest Team. 2018. The Everest Project. (2018). https:\/\/project- everest.github.io\/ .  The Project Everest Team. 2018. The Everest Project. (2018). https:\/\/project- everest.github.io\/ .","DOI":"10.1215\/00265667-4391548"},{"key":"e_1_2_2_42_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics. https: \/\/homotopytypetheory.org\/book","author":"Foundations Program The Univalent"},{"key":"e_1_2_2_44_1","unstructured":"Andrea Vezzosi. 2017. Streams for Cubical Type Theory. (2017). http:\/\/www.cse.chalmers.se\/~vezzosi\/streams- ctt.pdf  Andrea Vezzosi. 2017. Streams for Cubical Type Theory. (2017). http:\/\/www.cse.chalmers.se\/~vezzosi\/streams- ctt.pdf"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290317","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290317","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:02:07Z","timestamp":1750208527000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290317"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":43,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290317"],"URL":"https:\/\/doi.org\/10.1145\/3290317","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}