{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T12:38:41Z","timestamp":1740141521032,"version":"3.37.3"},"reference-count":55,"publisher":"Oxford University Press (OUP)","issue":"4","license":[{"start":{"date-parts":[[2017,1,17]],"date-time":"2017-01-17T00:00:00Z","timestamp":1484611200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"funder":[{"DOI":"10.13039\/501100003246","name":"NWO","doi-asserted-by":"publisher","award":["612.001.021"],"award-info":[{"award-number":["612.001.021"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]},{"name":"NWO-Veni","award":["639.021.231"],"award-info":[{"award-number":["639.021.231"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,6,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>We define notions of well-definedness and observational equivalence for programs of mixed inductive and coinductive types. These notions are defined by means of tests formulas which combine structural congruence for inductive types and modal logic for coinductive types. Tests also correspond to certain evaluation contexts. We define a program to be well-defined if it is strongly normalizing under all tests, and two programs are observationally equivalent if they satisfy the same tests.<\/jats:p>\n               <jats:p>We show that observational equivalence is sufficiently coarse to ensure that least and greatest fixed point types are initial algebras and final coalgebras, respectively. This yields inductive and coinductive proof principles for reasoning about program behaviour. On the other hand, we argue that observational equivalence does not identify too many terms, by showing that tests induce a topology that, on streams, coincides with usual topology induced by the prefix metric.<\/jats:p>\n               <jats:p>As one would expect, observational equivalence is, in general, undecidable, but in order to develop some practically useful heuristics we provide coinductive techniques for establishing observational normalization and observational equivalence, along with up-to techniques for enhancing these methods.<\/jats:p>","DOI":"10.1093\/logcom\/exv091","type":"journal-article","created":{"date-parts":[[2016,4,12]],"date-time":"2016-04-12T21:03:00Z","timestamp":1460494980000},"page":"419-468","source":"Crossref","is-referenced-by-count":0,"title":["Well-definedness and observational equivalence for inductive\u2013coinductive programs"],"prefix":"10.1093","volume":"29","author":[{"given":"Henning","family":"Basold","sequence":"first","affiliation":[{"name":"Radboud University and CWI Amsterdam"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Helle Hvid","family":"Hansen","sequence":"additional","affiliation":[{"name":"Delft University of Technology and CWI Amsterdam"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2019,7,8]]},"reference":[{"key":"2019070814453672600_B1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.4204\/EPTCS.77.1","article-title":"Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types","volume":"77","author":"Abel","year":"2012","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"2019070814453672600_B2","first-page":"185","article-title":"Wellfounded recursion with copatterns: a unified approach to termination and productivity","volume-title":"ICFP","author":"Abel","year":"2013"},{"key":"2019070814453672600_B3","first-page":"27","article-title":"Copatterns: programming infinite structures by observations","volume-title":"Proceedings of POPL","author":"Abel","year":"2013"},{"key":"2019070814453672600_B4","first-page":"65","article-title":"The lazy lambda calculus","volume-title":"Research Topics in Functional Programming","author":"Abramsky","year":"1990"},{"key":"2019070814453672600_B5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-7(1:15)2011","article-title":"Semantics of higher-order recursion schemes","volume":"7","author":"Ad\u00e1mek","year":"2011","journal-title":"Logical Methods in Computer Science"},{"key":"2019070814453672600_B6","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1145\/1292597.1292608","article-title":"Observational equality, now!","volume-title":"Proceedings of PLPV '07","author":"Altenkirch","year":"2007"},{"key":"2019070814453672600_B7","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1145\/2500365.2500597","article-title":"Productive coprogramming with guarded recursion","volume-title":"Proceedings of ICFP '13","author":"Atkey","year":"2013"},{"key":"2019070814453672600_B8","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139032636","volume-title":"Lambda calculus with types","author":"Barendregt","year":"2013"},{"volume-title":"The Lambda Calculus, Its Syntax and Semantics","year":"1985","author":"Barendregt","key":"2019070814453672600_B9"},{"key":"2019070814453672600_B10","first-page":"20:1","article-title":"Coinduction up-to in a fibrational setting","volume-title":"Proceedings of CSL-LICS '14","author":"Bonchi","year":"2014"},{"key":"2019070814453672600_B11","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1007\/978-3-540-73449-9_8","article-title":"Confluence of pattern-based calculi","volume-title":"Term Rewriting and Applications","author":"Cirstea","year":"2007"},{"key":"2019070814453672600_B12","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1017\/S0956796800001696","article-title":"A confluent reduction for the \u03bb-calculus with surjective pairing and terminal object","volume":"6","author":"Curien","year":"1996","journal-title":"Journal of Functional Programing"},{"key":"2019070814453672600_B13","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","article-title":"Testing equivalences for processes","volume":"34","author":"De Nicola","year":"1984","journal-title":"Theoretical Computer Science"},{"key":"2019070814453672600_B14","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/978-3-540-89439-1_6","article-title":"Data-oblivious stream productivity","volume-title":"Proceedings Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2008)","author":"Endrullis","year":"2008"},{"key":"2019070814453672600_B15","doi-asserted-by":"crossref","first-page":"765","DOI":"10.1016\/j.tcs.2009.10.014","article-title":"Productivity of stream definitions","volume":"411","author":"Endrullis","year":"2010","journal-title":"Theoretical Computer Science"},{"key":"2019070814453672600_B16","doi-asserted-by":"crossref","first-page":"3203","DOI":"10.1016\/j.tcs.2011.03.024","article-title":"Lazy productivity via termination","volume":"412","author":"Endrullis","year":"2011","journal-title":"Theoretical Computer Science"},{"key":"2019070814453672600_B17","first-page":"21","article-title":"Synthetic topology: of data types and classical spaces","volume":"87","author":"Escard\u00f3","year":"2004","journal-title":"ENTCS"},{"key":"2019070814453672600_B18","first-page":"248","article-title":"Cuts for circular proofs: semantics and cut-elimination","volume-title":"CSL","author":"Fortier","year":"2013"},{"key":"2019070814453672600_B19","first-page":"193","article-title":"Inductive and coinductive types with iteration and recursion","volume-title":"Proceedings of the 1992 Workshop on Types for Proofs and Programs, Bastad","author":"Geuvers","year":"1992"},{"key":"2019070814453672600_B20","first-page":"171","article-title":"Beta-eta equality for coproducts","volume-title":"Proceedings of TLCA'95","author":"Ghani","year":"1995"},{"key":"2019070814453672600_B21","article-title":"Representations of stream processors using nested fixed points","volume":"5","author":"Ghani","year":"2009","journal-title":"LMCS"},{"key":"2019070814453672600_B22","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/3-540-60579-7_3","article-title":"Codifying guarded definitions with recursive schemes","volume-title":"Selected Papers from the International Workshop on Types for Proofs and Programs","author":"Gim\u00e9nez","year":"1995"},{"volume-title":"Proofs and Types","year":"1989","author":"Girard","key":"2019070814453672600_B23"},{"key":"2019070814453672600_B24","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1016\/S1571-0661(04)80013-6","article-title":"Bisimilarity as a theory of functional programming","volume":"1","author":"Gordon","year":"1995","journal-title":"Electronic Notes in Theoretical Computer Science"},{"volume-title":"A Categorical Programming Language","year":"1987","author":"Hagino","key":"2019070814453672600_B25"},{"key":"2019070814453672600_B26","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1093\/acprof:oso\/9780198566519.003.0007","article-title":"Interactive programs and weakly final coalgebras in dependent type theory","volume-title":"From Sets and Types to Topology and Analysis towards Practicable Foundations for Constructive Mathematics","author":"Hancock","year":"2005"},{"key":"2019070814453672600_B27","article-title":"Stream differential equations: specification formats and solution methods","volume-title":"Technical Report FM-1404","author":"Hansen","year":"2014"},{"key":"2019070814453672600_B28","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1017\/S0960129500000372","article-title":"Categorical data types in parametric polymorphism","volume":"4","author":"Hasegawa","year":"1994","journal-title":"Mathematical Structures in Computer Science"},{"key":"2019070814453672600_B29","first-page":"198","article-title":"Equality in lazy computation systems","volume-title":"Fourth Annual Symposium on Logic in Computer Science, 1989. LICS '89, Proceedings","author":"Howe","year":"1989"},{"key":"2019070814453672600_B30","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1006\/inco.1996.0008","article-title":"Proving congruence of bisimulation in functional programming languages","volume":"124","author":"Howe","year":"1996","journal-title":"Information and Computation"},{"volume-title":"Categorical Logic and Type Theory","year":"1999","author":"Jacobs","key":"2019070814453672600_B31"},{"key":"2019070814453672600_B32","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1051\/ita:2001108","article-title":"Many-sorted coalgebraic modal logic: a model-theoretic study","volume":"35","author":"Jacobs","year":"2001","journal-title":"RAIRO - Theor. Inform. Appl."},{"key":"2019070814453672600_B33","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511792588.003","article-title":"An introduction to (co)algebras and (co)induction","volume":"52","author":"Jacobs","year":"2011","journal-title":"Advanced topics in bisimulation and coinduction"},{"key":"2019070814453672600_B34","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/j.entcs.2010.07.018","article-title":"Higher-order algebras and coalgebras from parameterized endofunctors","volume":"264","author":"Kim","year":"2010","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2019070814453672600_B35","doi-asserted-by":"crossref","first-page":"5043","DOI":"10.1016\/j.tcs.2011.03.023","article-title":"Bialgebras for structural operational semantics: an introduction","volume":"412","author":"Klin","year":"2011","journal-title":"TCS"},{"volume-title":"Finitary Coalgebraic Logics","year":"2006","author":"Kupke","key":"2019070814453672600_B36"},{"key":"2019070814453672600_B37","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1016\/S0049-237X(08)70727-4","article-title":"About {models} for intuitionistic type theories and the notion of definitional equality","volume-title":"3rd Scandinavian Logic Symposium","author":"Martin-L\u00f6f","year":"1975"},{"key":"2019070814453672600_B38","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(77)90053-6","article-title":"Fully abstract models of typed \u03bb-calculi","volume":"4","author":"Milner","year":"1977","journal-title":"Theoretical Computer Science"},{"key":"2019070814453672600_B39","doi-asserted-by":"crossref","DOI":"10.1145\/2603088.2603132","article-title":"A type theory for productive coprogramming via guarded recursion","volume-title":"Proceedings of LICS 2014","author":"Mogelberg","year":"2014"},{"key":"2019070814453672600_B40","doi-asserted-by":"crossref","first-page":"57","DOI":"10.4204\/EPTCS.32.5","article-title":"Resumptions, weak bisimilarity and big-step semantics for while with interactive I\/O: an exercise in mixed induction-coinduction","volume":"32","author":"Nakata","year":"2010","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"2019070814453672600_B41","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1017\/S0960129500003066","article-title":"Parametric polymorphism and operational equivalence","volume":"10","author":"Pitts","year":"2000","journal-title":"Mathematical Structures in Computer Science"},{"key":"2019070814453672600_B42","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/BFb0037118","article-title":"A logic for parametric polymorphism","volume-title":"Typed Lambda Calculi and Applications","author":"Plotkin","year":"1993"},{"key":"2019070814453672600_B43","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","article-title":"LCF considered as a programming language","volume":"5","author":"Plotkin","year":"1977","journal-title":"Theoretical Computer Science"},{"key":"2019070814453672600_B44","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/978-3-540-76637-7_24","article-title":"Complete lattices and up-to techniques","volume-title":"Programming Languages and Systems","author":"Pous","year":"2007"},{"key":"2019070814453672600_B45","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511792588.007","article-title":"Enhancements of the coinductive proof method","volume-title":"Advanced Topics in Bisimulation and Coinduction","author":"Pous","year":"2011"},{"key":"2019070814453672600_B46","article-title":"Enhancements of the bisimulation proof method","volume-title":"Advanced Topics in Bisimulation and Coinduction","author":"Pous","year":"2012"},{"key":"2019070814453672600_B47","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1016\/S1571-0661(05)80353-6","article-title":"Coalgebras and modal logic","volume":"33","author":"R\u00f6\u00dfiger","year":"2000","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2019070814453672600_B48","article-title":"Enhanced coalgebraic bisimulation","author":"Rot","year":"2014","journal-title":"MSCS"},{"key":"2019070814453672600_B49","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0304-3975(00)00056-6","article-title":"Universal coalgebra: a theory of systems","volume":"249","author":"Rutten","year":"2000","journal-title":"Theoretical Computer Science"},{"key":"2019070814453672600_B50","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0304-3975(02)00895-2","article-title":"Behavioural differential equations: a coinductive calculus of streams, automata, and power series","volume":"308","author":"Rutten","year":"2003","journal-title":"TCS"},{"key":"2019070814453672600_B51","first-page":"233","article-title":"Type-based productivity of stream definitions in the calculus of constructions","volume-title":"Proceedings of LICS 2013","author":"Sacchini","year":"2013"},{"key":"2019070814453672600_B52","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511777110","volume-title":"Introduction to Bisimulation and Coinduction","author":"Sangiorgi","year":"2011"},{"key":"2019070814453672600_B53","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-7(1:13)2011","article-title":"Relating coalgebraic notions of bisimulation","volume":"7","author":"Staton","year":"2011","journal-title":"Logical Methods in Computer Science"},{"key":"2019070814453672600_B54","first-page":"280","article-title":"Towards a mathematical operational semantics","volume-title":"Logic in Computer Science, 1997. LICS'97. Proceedings, 12th Annual IEEE Symposium","author":"Turi","year":"1997"},{"volume-title":"The Logical Basis of Evaluation Order and Pattern-Matching","year":"2009","author":"Zeilberger","key":"2019070814453672600_B55"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/29\/4\/419\/28917451\/exv091.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,20]],"date-time":"2019-09-20T06:42:46Z","timestamp":1568961766000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/29\/4\/419\/2917862"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,6]]},"references-count":55,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2019,7,8]]},"published-print":{"date-parts":[[2019,6,6]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exv091","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published-other":{"date-parts":[[2019,8,1]]},"published":{"date-parts":[[2019,6,6]]}}}