{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:31:38Z","timestamp":1770273098008,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642133206","type":"print"},{"value":"9783642133213","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-13321-3_8","type":"book-chapter","created":{"date-parts":[[2010,6,22]],"date-time":"2010-06-22T06:24:11Z","timestamp":1277187851000},"page":"100-118","source":"Crossref","is-referenced-by-count":25,"title":["Subtyping, Declaratively"],"prefix":"10.1007","author":[{"given":"Nils Anders","family":"Danielsson","sequence":"first","affiliation":[]},{"given":"Thorsten","family":"Altenkirch","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-540-76637-7_19","volume-title":"Programming Languages and Systems","author":"A. Abel","year":"2007","unstructured":"Abel, A.: Mixed inductive\/coinductive types and strong normalization. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol.\u00a04807, pp. 286\u2013301. Springer, Heidelberg (2007)"},{"issue":"1","key":"8_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0956796801004191","volume":"12","author":"A. Abel","year":"2002","unstructured":"Abel, A., Altenkirch, T.: A predicative analysis of structural recursion. Journal of Functional Programming\u00a012(1), 1\u201341 (2002)","journal-title":"Journal of Functional Programming"},{"key":"8_CR3","unstructured":"The Agda Team. The Agda Wiki (2010), http:\/\/wiki.portal.chalmers.se\/agda\/"},{"issue":"4","key":"8_CR4","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1145\/155183.155231","volume":"15","author":"R.M. Amadio","year":"1993","unstructured":"Amadio, R.M., Cardelli, L.: Subtyping recursive types. ACM Transactions on Programming Languages and Systems\u00a015(4), 575\u2013631 (1993)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"8_CR5","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1017\/S0960129503004122","volume":"14","author":"G. Barthe","year":"2004","unstructured":"Barthe, G., Frade, M.J., Gim\u00e9nez, E., Pinto, L., Uustalu, T.: Type-based termination of recursive definitions. Mathematical Structures in Computer Science\u00a014(1), 97\u2013141 (2004)","journal-title":"Mathematical Structures in Computer Science"},{"key":"8_CR6","unstructured":"Barwise, J.: Mixed Fixed Points. In: The Situation in Logic. CSLI Lecture Notes, vol.\u00a017, Center for the Study of Language and Information, Leland Stanford Junior University (1989)"},{"key":"8_CR7","series-title":"Studies in Logic and Practical Reasoning","doi-asserted-by":"publisher","DOI":"10.1016\/S1570-2464(07)80015-2","volume-title":"Handbook of Modal Logic","author":"J. Bradfield","year":"2007","unstructured":"Bradfield, J., Stirling, C.: Modal mu-calculi. In: Handbook of Modal Logic. Studies in Logic and Practical Reasoning, vol.\u00a03. Elsevier, Amsterdam (2007)"},{"issue":"4","key":"8_CR8","doi-asserted-by":"crossref","first-page":"309","DOI":"10.3233\/FI-1998-33401","volume":"33","author":"M. Brandt","year":"1998","unstructured":"Brandt, M., Henglein, F.: Coinductive axiomatization of recursive type equality and subtyping. Fundamenta Informaticae\u00a033(4), 309\u2013338 (1998)","journal-title":"Fundamenta Informaticae"},{"issue":"2","key":"8_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-1(2:1)2005","volume":"1","author":"V. Capretta","year":"2005","unstructured":"Capretta, V.: General recursion via coinductive types. Logical Methods in Computer Science\u00a01(2), 1\u201328 (2005)","journal-title":"Logical Methods in Computer Science"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-58085-9_72","volume-title":"Types for Proofs and Programs","author":"T. Coquand","year":"1994","unstructured":"Coquand, T.: Infinite objects in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol.\u00a0806, pp. 62\u201378. Springer, Heidelberg (1994)"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Inductive definitions, semantics and abstract interpretations. In: POPL\u00a0\u201992, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 83\u201394 (1992)","DOI":"10.1145\/143165.143184"},{"key":"8_CR12","unstructured":"Danielsson, N.A.: Code accompanying the paper (2010a), http:\/\/www.cs.nott.ac.uk\/~nad\/"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Danielsson, N.A.: Beating the productivity checker using embedded languages. Draft (2010b)","DOI":"10.4204\/EPTCS.43.3"},{"key":"8_CR14","unstructured":"Danielsson, N.A., Altenkirch, T.: Mixing induction and coinduction. Draft (2009)"},{"key":"8_CR15","unstructured":"de Vries, E.: Re: [Coq-Club] Adding (inductive) transitivity to weak bisimilarity not sound? (was: Need help with coinductive proof). Message to the Coq-Club mailing list (August 2009)"},{"issue":"6","key":"8_CR16","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1017\/S0956796802004318","volume":"12","author":"V. Gapeyev","year":"2002","unstructured":"Gapeyev, V., Levin, M.Y., Pierce, B.C.: Recursive subtyping revealed. Journal of Functional Programming\u00a012(6), 511\u2013548 (2002)","journal-title":"Journal of Functional Programming"},{"issue":"4","key":"8_CR17","first-page":"353","volume":"66","author":"J. Gibbons","year":"2005","unstructured":"Gibbons, J., Hutton, G.: Proof methods for corecursive programs. Fundamenta Informaticae\u00a066(4), 353\u2013366 (2005)","journal-title":"Fundamenta Informaticae"},{"key":"8_CR18","unstructured":"Gim\u00e9nez, E.: Un Calcul de Constructions Infinies et son Application \u00e0 la V\u00e9rification de Syst\u00e8mes Communicants. PhD thesis, Ecole Normale Sup\u00e9rieure de Lyon (1996)"},{"issue":"1-2","key":"8_CR19","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0304-3975(98)00353-3","volume":"228","author":"A.D. Gordon","year":"1999","unstructured":"Gordon, A.D.: Bisimilarity as a theory of functional programming. Theoretical Computer Science\u00a0228(1-2), 5\u201347 (1999)","journal-title":"Theoretical Computer Science"},{"key":"8_CR20","unstructured":"Hagino, T.: A Categorical Programming Language. PhD thesis, University of Edinburgh (1987)"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Hancock, P., Pattinson, D., Ghani, N.: Representations of stream processors using nested fixed points. Logical Methods in Computer Science\u00a05(3:9) (2009)","DOI":"10.2168\/LMCS-5(3:9)2009"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/BFb0026991","volume-title":"Category Theory and Computer Science","author":"U. Hensel","year":"1997","unstructured":"Hensel, U., Jacobs, B.: Proof principles for datatypes with iterated recursion. In: Moggi, E., Rosolini, G. (eds.) CTCS 1997. LNCS, vol.\u00a01290, pp. 220\u2013241. Springer, Heidelberg (1997)"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Hughes, J., Moran, A.: Making choices lazily. In: FPCA\u00a0\u201995, Proceedings of the seventh international conference on Functional programming languages and computer architecture, pp. 108\u2013119 (1995)","DOI":"10.1145\/224164.224191"},{"issue":"1","key":"8_CR24","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1017\/S0960129500000657","volume":"5","author":"D. Kozen","year":"1995","unstructured":"Kozen, D., Palsberg, J., Schwartzbach, M.I.: Efficient recursive subtyping. Mathematical Structures in Computer Science\u00a05(1), 113\u2013125 (1995)","journal-title":"Mathematical Structures in Computer Science"},{"issue":"2","key":"8_CR25","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1016\/j.ic.2007.12.004","volume":"207","author":"X. Leroy","year":"2009","unstructured":"Leroy, X., Grall, H.: Coinductive big-step operational semantics. Information and Computation\u00a0207(2), 284\u2013304 (2009)","journal-title":"Information and Computation"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Levy, P.B.: Infinitary Howe\u2019s method. In: Proceedings of the Eighth Workshop on Coalgebraic Methods in Computer Science (CMCS 2006). ENTCS, vol.\u00a0164, pp. 85\u2013104 (2006)","DOI":"10.1016\/j.entcs.2006.06.006"},{"key":"8_CR27","unstructured":"Mendler, P.F.: Inductive Definition in Type Theory. PhD thesis, Cornell University (1988)"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Milner, R.: Operational and algebraic semantics of concurrent processes. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics. The MIT Press and Elsevier (1990)","DOI":"10.1016\/B978-0-444-88074-1.50024-X"},{"issue":"1","key":"8_CR29","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/0304-3975(91)90033-X","volume":"87","author":"R. Milner","year":"1991","unstructured":"Milner, R., Tofte, M.: Co-induction in relational semantics. Theoretical Computer Science\u00a087(1), 209\u2013220 (1991)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"8_CR30","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1017\/S095679689900341X","volume":"9","author":"O. M\u00fcller","year":"1999","unstructured":"M\u00fcller, O., Nipkow, T., von Oheimb, D., Slotosch, O.: HOLCF = HOL + LCF. Journal of Functional Programming\u00a09(2), 191\u2013223 (1999)","journal-title":"Journal of Functional Programming"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-642-03359-9_26","volume-title":"Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009","author":"K. Nakata","year":"2009","unstructured":"Nakata, K., Uustalu, T.: Trace-based coinductive operational semantics for While; Big-step and small-step, relational and functional styles. In: Urban, C. (ed.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 375\u2013390. Springer, Heidelberg (2009)"},{"key":"8_CR32","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology and G\u00f6teborg University (2007)"},{"key":"8_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"504","DOI":"10.1007\/3-540-10007-5_47","volume-title":"Abstract Software Specifications","author":"D. Park","year":"1980","unstructured":"Park, D.: On the semantics of fair parallelism. In: Bjorner, D. (ed.) Abstract Software Specifications. LNCS, vol.\u00a086, pp. 504\u2013526. Springer, Heidelberg (1980)"},{"key":"8_CR34","unstructured":"Raffalli, C.: L\u2019Arithm\u00e9tique Fonctionnelle du Second Ordre avec Points Fixes. PhD thesis, Universit\u00e9 Paris VII (1994)"},{"key":"8_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/BFb0084781","volume-title":"CONCUR \u201992","author":"D. Sangiorgi","year":"1992","unstructured":"Sangiorgi, D., Milner, R.: The problem of \u201cweak bisimulation up to\u201d. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol.\u00a0630, pp. 32\u201346. Springer, Heidelberg (1992)"},{"issue":"7","key":"8_CR36","first-page":"751","volume":"10","author":"D.A. Turner","year":"2004","unstructured":"Turner, D.A.: Total functional programming. Journal of Universal Computer Science\u00a010(7), 751\u2013768 (2004)","journal-title":"Journal of Universal Computer Science"},{"key":"8_CR37","unstructured":"Wadler, P., Taha, W., MacQueen, D.: How to add laziness to a strict language, without even being odd. In: Proceedings of the 1998 ACM SIGPLAN Workshop on ML (1998)"}],"container-title":["Lecture Notes in Computer Science","Mathematics of Program Construction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-13321-3_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T03:04:53Z","timestamp":1606187093000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-13321-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642133206","9783642133213"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-13321-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}