{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T06:43:34Z","timestamp":1725691414490},"publisher-location":"Dordrecht","reference-count":49,"publisher":"Springer Netherlands","isbn-type":[{"type":"print","value":"9789400744349"},{"type":"electronic","value":"9789400744356"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-94-007-4435-6_16","type":"book-chapter","created":{"date-parts":[[2012,7,10]],"date-time":"2012-07-10T14:08:37Z","timestamp":1341929317000},"page":"351-369","source":"Crossref","is-referenced-by-count":6,"title":["Coalgebras as Types Determined by Their Elimination Rules"],"prefix":"10.1007","author":[{"given":"Anton","family":"Setzer","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,6,7]]},"reference":[{"key":"16_CR1","volume-title":"Non-wellfounded set theory, CSLI lecture notes","author":"P Aczel","year":"1988","unstructured":"Aczel, P. 1988. Non-wellfounded set theory, CSLI lecture notes, vol.\u00a014, xx+137. Stanford: Stanford University, Center for the Study of Language and Information."},{"unstructured":"Agda. 2011 Email list archive. Available at https:\/\/lists.chalmers.se\/pipermail\/agda\/ .","key":"16_CR2"},{"unstructured":"Altenkirch, T. 2004. Codata. Talk given at the TYPES workshop in Jouy-en-Josas. Available from http:\/\/www.cs.nott.ac.uk\/~txa\/talks\/types04.pdf , Dec 2004.","key":"16_CR3"},{"unstructured":"Altenkirch, T., and N.A. Danielsson. 2010. Termination checking nested inductive and coinductive types. In Proceedings of workshop on partiality and recursion in interactive theorem provers, PAR\u201910, Edinburgh.","key":"16_CR4"},{"unstructured":"Bertot, Y. 2006. CoInduction in Coq. Available from http:\/\/arxiv.org\/abs\/cs\/0603119 , Mar 2006.","key":"16_CR5"},{"key":"16_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive theorem proving and program development. Coq\u2019Art: The calculus of inductive constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., and P. Cast\u00e9ran. 2004. Interactive theorem proving and program development. Coq\u2019Art: The calculus of inductive constructions. Berlin\/New York: Springer."},{"unstructured":"Cockett, J., and D. Spencer. 1992. Strong categorical datatypes I. In Category theory 1991: proceedings of an international summer category theory meeting, held June 23\u201330, 1991, vol.\u00a013, ed. R.A.G. Seely, 141. Providence: American Mathematical Society.","key":"16_CR7"},{"issue":"1\u20132","key":"16_CR8","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/0304-3975(94)00099-5","volume":"139","author":"JRB Cockett","year":"1995","unstructured":"Cockett, J.R.B., and D. Spencer. 1995. Strong categorical datatypes II: A term logic for categorical programming. Theoretical Computer Science 139(1\u20132): 69\u2013113.","journal-title":"Theoretical Computer Science"},{"unstructured":"Cockett, R., and T. Fukushima. 1992. About charity. Technical report, Department of Computer Science, The University of Calgary, June 1992. Yellow series report no. 92\/480\/18.","key":"16_CR9"},{"key":"16_CR10","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-58085-9_72","volume-title":"Types for proofs and programs, Lecture notes in computer science","author":"T Coquand","year":"1994","unstructured":"Coquand, T. 1994. Infinite objects in type theory. In Types for proofs and programs, Lecture notes in computer science, vol. 806, ed. H. Barendregt and T. Nipkow, 62\u201378. Berlin: Springer"},{"unstructured":"Danielsson, N.A. 2008. Codata oddity. Email posted on the Agda email list. Available from http:\/\/thread.gmane.org\/gmane.comp.lang.agda\/226 .","key":"16_CR11"},{"issue":"4","key":"16_CR12","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1023\/A:1004881914911","volume":"29","author":"GF D\u00edez","year":"2000","unstructured":"D\u00edez, G.F. 2000. Five observations concerning the intended meaning of the intuitionistic logical constants. Journal of Philosophical Logic 29(4): 409\u2013424.","journal-title":"Journal of Philosophical Logic"},{"key":"16_CR13","doi-asserted-by":"crossref","first-page":"37","DOI":"10.2478\/disp-2002-0003","volume":"12","author":"GF D\u00edez","year":"2002","unstructured":"D\u00edez, G.F. 2002. The logic of constructivism. Disputatio 12: 37\u201341.","journal-title":"Disputatio"},{"unstructured":"D\u00edez, G.F. 2003. Is the language of intuitionistic mathematics adequate for intuitionistic purposes? L&PS - Logic and Philosophy of Science 1(1).","key":"16_CR14"},{"key":"16_CR15","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198505242.001.0001","volume-title":"Elements of intuitionism. Oxford logic guides","author":"M Dummett","year":"2000","unstructured":"Dummett, M. 2000. Elements of intuitionism. Oxford logic guides, 2nd ed. New York: Oxford University Press.","edition":"2"},{"key":"16_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0168-0072(02)00096-9","volume":"124","author":"P Dybjer","year":"2003","unstructured":"Dybjer, P., and A. Setzer. 2003. Induction\u2013recursion and initial algebras. Annals of Pure and Applied Logic 124: 1\u201347.","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1\u201349","key":"16_CR17","first-page":"2006","volume":"66","author":"P Dybjer","year":"2006","unstructured":"Dybjer, P., and A. Setzer. 2006. Indexed induction\u2013recursion. Journal of Logic and Algebraic Programming 66: 1\u201349, 2006.","journal-title":"Journal of Logic and Algebraic Programming"},{"unstructured":"Gim\u00e9nez, C.E. 1996. Un calcul de constructions infinies et son application \u00e0 la v\u00e9rification de syst\u00e8mes communicants. (English: A calculus of infinite constructions and its application to the verification of communicating systems). Ph.D. thesis, Ecole normale sup\u00e9rieure de Lyon, Lyon, France.","key":"16_CR18"},{"doi-asserted-by":"crossref","unstructured":"Gim\u00e9nez, E. 1994. Codifying guarded definitions with recursive schemes. In Proceedings of the 1994 workshop on types for proofs and programs, Bastad, LNCS No. 996, 39\u201359. Springer.","key":"16_CR19","DOI":"10.1007\/3-540-60579-7_3"},{"unstructured":"Hagino, T. 1987. A categorical programming language. Ph.D. thesis, Laboratory for Foundations of Computer Science, University of Edinburgh. Available from http:\/\/www.tom.sfc.keio.ac.jp\/~hagino\/thesis.pdf .","key":"16_CR20"},{"issue":"6","key":"16_CR21","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1016\/S0747-7171(89)80065-3","volume":"8","author":"T Hagino","year":"1989","unstructured":"Hagino, T. 1989. Codatatypes in ml. Journal of Symbolic Computation 8(6): 629\u2013650.","journal-title":"Journal of Symbolic Computation"},{"unstructured":"Hancock, P., and A. Setzer. 1999. The IO monad in dependent type theory. In Electronic proceedings of the workshop on dependent types in programming, G\u00f6teborg, 27\u201328, Mar 1999. Available at http:\/\/www.md.chalmers.se\/Cs\/Research\/Semantics\/APPSEM\/dtp99.html .","key":"16_CR22"},{"key":"16_CR23","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/3-540-44622-2_21","volume-title":"Computer science logic: 14th international workshop, CSL 2000. Lecture notes in computer science, Vol. 1862","author":"P Hancock","year":"2000","unstructured":"Hancock, P., and A. Setzer. 2000a. Interactive programs in dependent type theory. In Computer science logic: 14th international workshop, CSL 2000. Lecture notes in computer science, Vol.\u00a01862, ed. P. Clote and H. Schwichtenberg, 317\u2013331. Berlin: Springer."},{"unstructured":"Hancock, P., and A. Setzer. 2000b. Specifying interactions with dependent types. In Workshop on subtyping and dependent types in programming, Portugal, 7 July 2000. Electronic proceedings, available at http:\/\/www-sop.inria.fr\/oasis\/DTP00\/Proceedings\/proceedings.html .","key":"16_CR24"},{"unstructured":"Hancock, P., and A. Setzer. 2004. Interactive programs and weakly final coalgebras (extended version). In Dependently typed programming, ed. T. Altenkirch, M. Hofmann, and J.\u00a0Hughes, number 04381 in Dagstuhl Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss Dagstuhl, Germany. Available at http:\/\/drops.dagstuhl.de\/opus\/ .","key":"16_CR25"},{"doi-asserted-by":"crossref","unstructured":"Hancock, P., and A. Setzer. 2005. Guarded induction and weakly final coalgebras in dependent type theory. In From sets and types to topology and analysis. Towards practicable foundations for constructive mathematics, ed. L. Crosilla and P. Schuster, 115\u2013134, Oxford: Clarendon Press.","key":"16_CR26","DOI":"10.1093\/acprof:oso\/9780198566519.003.0007"},{"key":"16_CR27","first-page":"83","volume-title":"Object orientation with parallelism and persistence","author":"B Jacobs","year":"1995","unstructured":"Jacobs, B. 1995. Objects and classes, co-algebraically. In Object orientation with parallelism and persistence, ed. B. Freitag, C.B. Jones, C. Lengauer, and H.-J. Schek, 83\u2013103. Boston: Kluwer."},{"doi-asserted-by":"crossref","unstructured":"Jacobs, B. 1998. Coalgebraic reasoning about classes in object-oriented languages. Electronical Notes in Computer Science 11: 231\u2013242. Special issue on the workshop coalgebraic methods in computer science (CMCS 1998).","key":"16_CR28","DOI":"10.1016\/S1571-0661(04)00061-1"},{"key":"16_CR29","volume-title":"Categorical logic and type theory, Number 141 in studies in logic and the foundations of mathematics","author":"B Jacobs","year":"1999","unstructured":"Jacobs, B. 1999. Categorical logic and type theory, Number 141 in studies in logic and the foundations of mathematics. Amsterdam: North Holland."},{"unstructured":"Jacobs, B. 2005. Introduction to coalgebra. Towards mathematics of states and oberservations. Available at http:\/\/www.cs.ru.nl\/B.Jacobs\/CLG\/JacobsCoalgebraIntro.pdf .","key":"16_CR30"},{"key":"16_CR31","first-page":"62","volume":"62","author":"B Jacobs","year":"1997","unstructured":"Jacobs, B., and J. Rutten. 1997. A tutorial on (co)algebras and (co)induction. EATCS Bulletin 62: 62\u2013222.","journal-title":"EATCS Bulletin"},{"doi-asserted-by":"crossref","unstructured":"Leclerc, F., and C. Paulin-Mohring. Programming with streams in Coq. A case study: The sieve of eratosthenes. In Types for proofs and programs, Lecture notes in computer science, vol. 806, ed. H. Barendregt and T. Nipkow, 191\u2013212. Berlin\/Heidelberg: Springer.","key":"16_CR32","DOI":"10.1007\/3-540-58085-9_77"},{"issue":"1","key":"16_CR33","first-page":"93","volume":"24","author":"P Martin-L\u00f6f","year":"1972","unstructured":"Martin-L\u00f6f, P. 1972. Infinite terms and a system of natural deduction. Compositio Mathematica 24(1): 93\u2013103.","journal-title":"Compositio Mathematica"},{"key":"16_CR34","volume-title":"Intuitionistic type theory","author":"P Martin-L\u00f6f","year":"1984","unstructured":"Martin-L\u00f6f, P. 1984. Intuitionistic type theory. Naples: Bibliopolis."},{"key":"16_CR35","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/BF00484985","volume":"73","author":"P Martin-L\u00f6f","year":"1987","unstructured":"Martin-L\u00f6f, P. 1987. Truth of a proposition, evidence of a judgement, validity of a proof. Synthese 73: 407\u2013420.","journal-title":"Synthese"},{"issue":"1","key":"16_CR36","first-page":"11","volume":"1","author":"P Martin-L\u00f6f","year":"1996","unstructured":"Martin-L\u00f6f, P. 1996. On the meaning of the logical constants and the justification of the logical laws. Nordic Journal of Philosophical Logic 1(1): 11\u201360.","journal-title":"Nordic Journal of Philosophical Logic"},{"unstructured":"Martin-L\u00f6f, P. 1998. An intuitionistic theory of types. In Twenty-five years of constructive type theory, ed. G. Sambin and J. Smith, 127\u2013172. Oxford: Oxford University Press. Reprinted version of an unpublished report from 1972.","key":"16_CR37"},{"key":"16_CR38","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/978-3-642-03741-2_9","volume-title":"Proceedings of the 3rd international conference on algebra and coalgebra in computer science, CALCO\u201909, Lecture notes in computer science","author":"C McBride","year":"2009","unstructured":"McBride, C. 2009. Let\u2019s see how things unfold: Reconciling the infinite with the intensional. In Proceedings of the 3rd international conference on algebra and coalgebra in computer science, CALCO\u201909, Lecture notes in computer science, ed. A. Kurz, M. Lenisa, and A. Tarlecki, 113\u2013126. Berlin\/Heidelberg: Springer."},{"key":"16_CR39","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1352582.1352591","volume":"9","author":"A. Nanevski","year":"2008","unstructured":"Nanevski, A., F. Pfenning, and B. Pientka. 2008. Contextual modal type theory. ACM Transactions on Computational Logic 9:23:1\u201323:49.","journal-title":"ACM Transactions on Computational Logic"},{"key":"16_CR40","volume-title":"Programming in Martin-L\u00f6f\u2019s type theory: An introduction","author":"B Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., K. Petersson, and J.M. Smith. 1990. Programming in Martin-L\u00f6f\u2019s type theory: An introduction. New York: Oxford University Press."},{"unstructured":"Norell, U. 2007. Towards a practical programming language based on dependent type theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 G\u00f6teborg.","key":"16_CR41"},{"unstructured":"Oury, N. 2008. Coinductive types and type preservation. Email posted 6 June 2008 at science.mathematics.logic.coq.club. Available at https:\/\/sympa-roc.inria.fr\/wws\/arc\/coq-club\/2008-06\/msg00022.html?checked_cas=2 .","key":"16_CR42"},{"key":"16_CR43","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1007\/3-540-58156-1_11","volume-title":"Automated deduction CADE-12, Lecture notes in computer science","author":"L Paulson","year":"1994","unstructured":"Paulson, L. 1994. A fixedpoint approach to implementing (Co) inductive definitions. In Automated deduction CADE-12, Lecture notes in computer science, vol. 814, ed. A. Bundy, 148\u2013161. Berlin\/Heidelberg: Springer."},{"doi-asserted-by":"crossref","unstructured":"Setzer, A. 2008. Universes in type theory part I \u2013 Inaccessibles and Mahlo. In Logic colloquium \u201904, Lecture notes in logic 29, ed. A. Andretta, K. Kearnes, and D. Zambella, Association of Symbolic Logic, 123\u2013156. Cambridge: Cambridge University Press.","key":"16_CR44","DOI":"10.1017\/CBO9780511721151.009"},{"key":"16_CR45","volume-title":"Why codata should be replaced by coalgebras","author":"A Setzer","year":"2011","unstructured":"Setzer, A. 2011. Why codata should be replaced by coalgebras. In preparation."},{"key":"16_CR46","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BF00247187","volume":"12","author":"G Sundholm","year":"1983","unstructured":"Sundholm, G. 1983. Constructions, proofs and the meaning of logical constants. Journal of Philosophical Logic 12: 151\u2013172. 10.1007\/BF00247187.","journal-title":"Journal of Philosophical Logic"},{"doi-asserted-by":"crossref","unstructured":"Telford, A. and D. Turner. 1997. Ensuring streams flow. In Algebraic methodology and software technology: 6th international conference, AMAST\u201996 Sydney, December 13 \u2013 17, 1997, Lecture notes in computer science, ed. M. Johnson, 509\u2013523, 1349. Berlin: Springer.","key":"16_CR47","DOI":"10.1007\/BFb0000493"},{"doi-asserted-by":"crossref","unstructured":"Turner, D. 1995. Elementary strong functional programming. Funtional Programming Languages in Education 1\u201313.","key":"16_CR48","DOI":"10.1007\/3-540-60675-0_35"},{"issue":"7","key":"16_CR49","first-page":"751","volume":"10","author":"DA Turner","year":"2004","unstructured":"Turner, D.A. 2004. Total functional programming. Journal of Universal Computer Science 10(7): 751\u2013768.","journal-title":"Journal of Universal Computer Science"}],"container-title":["Epistemology versus Ontology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-94-007-4435-6_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,26]],"date-time":"2024-04-26T17:29:08Z","timestamp":1714152548000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-94-007-4435-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9789400744349","9789400744356"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-94-007-4435-6_16","relation":{},"subject":[],"published":{"date-parts":[[2012]]}}}