{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:14Z","timestamp":1775790794428,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642389450","type":"print"},{"value":"9783642389467","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38946-7_13","type":"book-chapter","created":{"date-parts":[[2013,5,27]],"date-time":"2013-05-27T01:30:38Z","timestamp":1369618238000},"page":"156-172","source":"Crossref","is-referenced-by-count":15,"title":["Small Induction Recursion"],"prefix":"10.1007","author":[{"given":"Peter","family":"Hancock","sequence":"first","affiliation":[]},{"given":"Conor","family":"McBride","sequence":"additional","affiliation":[]},{"given":"Neil","family":"Ghani","sequence":"additional","affiliation":[]},{"given":"Lorenzo","family":"Malatesta","sequence":"additional","affiliation":[]},{"given":"Thorsten","family":"Altenkirch","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.tcs.2005.06.002","volume":"342","author":"M. Abbott","year":"2005","unstructured":"Abbott, M., Altenkirch, T., Ghani, N.: Containers. Constructing Strictly Positive Types. TCS\u00a0342, 3\u201327 (2005)","journal-title":"TCS"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Altenkirch, T., Morris, P.: Indexed containers. In: Procs. of the 24th Annual IEEE Symposium on Logic in Computer Science (LICS 2009). IEEE Computer Society (2009)","DOI":"10.1109\/LICS.2009.33"},{"key":"13_CR3","doi-asserted-by":"publisher","first-page":"739","DOI":"10.1016\/S0049-237X(08)71120-0","volume-title":"Handbook of Mathematical Logic","author":"P. Aczel","year":"1977","unstructured":"Aczel, P.: An introduction to inductive definition. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 739\u2013782. North-Holland, Amsterdam (1977)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/3-540-44755-5_10","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Bove","year":"2001","unstructured":"Bove, A., Capretta, V.: Nested General Recursion and Partiality in Type Theory. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 121\u2013135. Springer, Heidelberg (2001)"},{"key":"13_CR5","unstructured":"Clairambault, P., Dybjer, P.: The Biequivalence of Locally Cartesian Closed Category and Martin L\u00f6f Type Theories. Arxiv:1112.3456v1 [cs.LO] (December 15, 2011)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1007\/3-540-58715-2_114","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"T. Coquand","year":"1994","unstructured":"Coquand, T., Dybjer, P.: Inductive Definitions and Type Theory an Introduction. In: Thiagarajan, P.S. (ed.) FSTTCS 1994. LNCS, vol.\u00a0880, pp. 60\u201376. Springer, Heidelberg (1994)"},{"issue":"1-2","key":"13_CR7","doi-asserted-by":"crossref","first-page":"51","DOI":"10.3233\/FI-1993-191-204","volume":"19","author":"P.-L. Curien","year":"1993","unstructured":"Curien, P.-L.: Substitution up to isomorphism. Fundamenta Informaticae\u00a019(1-2), 51\u201386 (1993)","journal-title":"Fundamenta Informaticae"},{"issue":"2","key":"13_CR8","doi-asserted-by":"publisher","first-page":"525","DOI":"10.2307\/2586554","volume":"65","author":"P. Dybjer","year":"2000","unstructured":"Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic\u00a065(2), 525\u2013549 (2000)","journal-title":"Journal of Symbolic Logic"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/3-540-48959-2_11","volume-title":"Typed Lambda Calculi and Applications","author":"P. Dybjer","year":"1999","unstructured":"Dybjer, P., Setzer, A.: A Finite Axiomatization of Inductive-Recursive Definitions. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol.\u00a01581, pp. 129\u2013146. Springer, Heidelberg (1999)"},{"key":"13_CR10","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., Setzer, A.: Induction-recursion and initial algebras. Annales of Pure and Applied Logic\u00a0124, 1\u201347 (2003)","journal-title":"Annales of Pure and Applied Logic"},{"issue":"1","key":"13_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jlap.2005.07.001","volume":"66","author":"P. Dybjer","year":"2006","unstructured":"Dybjer, P., Setzer, A.: Indexed Induction-Recursion. Journal of Logic and Algebraic Programming\u00a066(1), 1\u201349 (2006)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"13_CR12","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":"13_CR13","unstructured":"Gambino, N., Kock, J.: Polynomial functors and polynomial monads. Arxiv:0906.4931v2 [math.CT] (March 6, 2010)"},{"key":"13_CR14","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":"13_CR15","unstructured":"Kock, J.: Notes on Polynomial functors, http:\/\/www.mat.uab.es\/~kock\/cat\/polynomial.html"},{"key":"13_CR16","volume-title":"Categories for the working mathematician","author":"S. Mac Lane","year":"1998","unstructured":"Mac Lane, S.: Categories for the working mathematician, 2nd edn. Springer, New York (1998)","edition":"2"},{"key":"13_CR17","first-page":"73","volume-title":"Logic Colloquium 1973","author":"P. Martin-L\u00f6f","year":"1973","unstructured":"Martin-L\u00f6f, P.: An intuitionistic theory of types: Predicative part. In: Logic Colloquium 1973, pp. 73\u2013118. North-Holland, Amsterdam (1973)"},{"key":"13_CR18","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":"13_CR19","doi-asserted-by":"crossref","unstructured":"Seely, R.A.G.: Locally cartesian closed categories and type theory. Math. Proc. Cambridge Philos. Soc.\u00a0(95), 33\u201348 (1984)","DOI":"10.1017\/S0305004100061284"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38946-7_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,22]],"date-time":"2022-02-22T22:45:48Z","timestamp":1645569948000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38946-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642389450","9783642389467"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38946-7_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}