{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:02Z","timestamp":1780994702384,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540228493","type":"print"},{"value":"9783540278368","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27836-8_8","type":"book-chapter","created":{"date-parts":[[2010,9,15]],"date-time":"2010-09-15T18:53:21Z","timestamp":1284576801000},"page":"59-71","source":"Crossref","is-referenced-by-count":15,"title":["Representing Nested Inductive Types Using W-Types"],"prefix":"10.1007","author":[{"given":"Michael","family":"Abbott","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thorsten","family":"Altenkirch","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Neil","family":"Ghani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Abbott, M.: Categories of Containers. PhD thesis, University of Leicester (2003)","DOI":"10.1007\/3-540-36576-1_2"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/3-540-36576-1_2","volume-title":"Foundations of Software Science and Computational Structures","author":"M. Abbott","year":"2003","unstructured":"Abbott, M., Altenkirch, T., Ghani, N.: Categories of containers. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol.\u00a02620, pp. 23\u201338. Springer, Heidelberg (2003)"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Abbott, M., Altenkirch, T., Ghani, N.: Representing strictly positive types. Presented at APPSEM annual meeting, invited for submission to Theoretical Computer Science (2004)","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/3-540-44557-9_2","volume-title":"Types for Proofs and Programs","author":"A. Abel","year":"2000","unstructured":"Abel, A., Altenkirch, T.: Apredicative strong normalisation proof for a \u03bb-calculus with interleaving inductive types. In: Coquand, T., Nordstr\u00f6m, B., Dybjer, P., Smith, J. (eds.) TYPES 1999. LNCS, vol.\u00a01956, pp. 21\u201340. Springer, Heidelberg (2000)"},{"key":"8_CR5","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/S0304-3975(96)00145-4","volume":"176","author":"P. Dybjer","year":"1997","unstructured":"Dybjer, P.: Representing inductively defined sets by wellorderings in Martin-L\u00f6f\u2019s type theory. Theoretical Computer Science\u00a0176, 329\u2013335 (1997)","journal-title":"Theoretical Computer Science"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Dybjer, P., Setzer, A.: A finite axiomatization of inductive-recursive definitions. In: Typed Lambda Calculus and Applications, pp. 129\u2013146 (1999)","DOI":"10.1007\/3-540-48959-2_11"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/3-540-45504-3_7","volume-title":"Proof Theory in Computer Science","author":"P. Dybjer","year":"2001","unstructured":"Dybjer, P., Setzer, A.: Indexed induction-recursion. In: Kahle, R., Schroeder-Heister, P., St\u00e4rk, R.F. (eds.) PTCS 2001. LNCS, vol.\u00a02183, p. 93. Springer, Heidelberg (2001)"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-540-24849-1_14","volume-title":"Types for Proofs and Programs","author":"N. Gambino","year":"2004","unstructured":"Gambino, N., Hyland, M.: Wellfounded trees and dependent polynomial functors. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 210\u2013225. Springer, Heidelberg (2004)"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/BFb0022273","volume-title":"Computer Science Logic","author":"M. Hofmann","year":"1995","unstructured":"Hofmann, M.: On the interpretation of type theory in locally cartesian closed categories. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol.\u00a0933, pp. 427\u2013441. Springer, Heidelberg (1995)"},{"key":"8_CR10","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Categorical Logic and Type Theory","author":"B. Jacobs","year":"1999","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol.\u00a0141. Elsevier, Amsterdam (1999)"},{"key":"8_CR11","volume-title":"Topos Theory","author":"P.T. Johnstone","year":"1977","unstructured":"Johnstone, P.T.: Topos Theory. Academic Press, London (1977)"},{"key":"8_CR12","volume-title":"Intuitionistic Type Theory","author":"P. Martin-L\u00f6f","year":"1984","unstructured":"Martin-L\u00f6f, P.: Intuitionistic Type Theory. Bibliopolis, Napoli (1984)"},{"key":"8_CR13","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/S0168-0072(00)00012-9","volume":"104","author":"I. Moerdijk","year":"2000","unstructured":"Moerdijk, I., Palmgren, E.: Wellfounded trees in categories. Annals of Pure and Applied Logic\u00a0104, 189\u2013218 (2000)","journal-title":"Annals of Pure and Applied Logic"},{"key":"8_CR14","series-title":"International Series of Monographs on Computer Science","volume-title":"Programming in Martin-L\u00f6f\u2019s Type Theory","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.M.: Programming in Martin-L\u00f6f\u2019s Type Theory. International Series of Monographs on Computer Science, vol.\u00a07. Oxford University Press, Oxford (1990)"},{"key":"8_CR15","series-title":"Progress in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0433-6","volume-title":"Semantics of Type Theory","author":"T. Streicher","year":"1991","unstructured":"Streicher, T.: Semantics of Type Theory. Progress in Theoretical Computer Science. Birkh\u00e4user, Basel (1991)"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27836-8_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,9]],"date-time":"2021-11-09T20:30:23Z","timestamp":1636489823000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27836-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540228493","9783540278368"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27836-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}