{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:59:47Z","timestamp":1759147187013},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642152047"},{"type":"electronic","value":"9783642152054"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15205-4_35","type":"book-chapter","created":{"date-parts":[[2010,8,13]],"date-time":"2010-08-13T14:48:24Z","timestamp":1281710904000},"page":"454-468","source":"Crossref","is-referenced-by-count":7,"title":["Inductive-Inductive Definitions"],"prefix":"10.1007","author":[{"given":"Fredrik","family":"Nordvall Forsberg","sequence":"first","affiliation":[]},{"given":"Anton","family":"Setzer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"35_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-48167-2_1","volume-title":"Types for Proofs and Programs","author":"P. Aczel","year":"1999","unstructured":"Aczel, P.: On relating type theories and set theories. In: Altenkirch, T., Naraschewski, W., Reus, B. (eds.) TYPES 1998. LNCS, vol.\u00a01657, pp. 1\u201318. Springer, Heidelberg (1999)"},{"issue":"1","key":"35_CR2","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/BF01887198","volume":"1","author":"R. Backhouse","year":"1989","unstructured":"Backhouse, R., Chisholm, P., Malcolm, G., Saaman, E.: Do-it-yourself type theory. Formal Aspects of Computing\u00a01(1), 19\u201384 (1989)","journal-title":"Formal Aspects of Computing"},{"key":"35_CR3","first-page":"265","volume":"10","author":"M. Benke","year":"2003","unstructured":"Benke, M., Dybjer, P., Jansson, P.: Universes for generic programs and proofs in dependent type theory. Nordic Journal of Computing\u00a010, 265\u2013269 (2003)","journal-title":"Nordic Journal of Computing"},{"key":"35_CR4","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.entcs.2008.12.114","volume":"228","author":"J. Chapman","year":"2009","unstructured":"Chapman, J.: Type theory should eat itself. Electronic Notes in Theoretical Computer Science\u00a0228, 21\u201336 (2009)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"35_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-74464-1_7","volume-title":"Types for Proofs and Programs","author":"N. Danielsson","year":"2007","unstructured":"Danielsson, N.: A formalisation of a dependently typed language as an inductive-recursive family. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 93\u2013109. Springer, Heidelberg (2007)"},{"issue":"4","key":"35_CR6","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/BF01211308","volume":"6","author":"P. Dybjer","year":"1994","unstructured":"Dybjer, P.: Inductive families. Formal aspects of computing\u00a06(4), 440\u2013465 (1994)","journal-title":"Formal aspects of computing"},{"key":"35_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1007\/3-540-61780-9_66","volume-title":"Types for Proofs and Programs","author":"P. Dybjer","year":"1996","unstructured":"Dybjer, P.: Internal type theory. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol.\u00a01158, pp. 120\u2013134. Springer, Heidelberg (1996)"},{"issue":"2","key":"35_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":"35_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. (ed.) TLCA 1999. LNCS, vol.\u00a01581, pp. 129\u2013146. Springer, Heidelberg (1999)"},{"issue":"1-3","key":"35_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\u2013recursion and initial algebras. Annals of Pure and Applied Logic\u00a0124(1-3), 1\u201347 (2003)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1","key":"35_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\u2013recursion. Journal of logic and algebraic programming\u00a066(1), 1\u201349 (2006)","journal-title":"Journal of logic and algebraic programming"},{"key":"35_CR12","unstructured":"Martin-L\u00f6f, P.: Intuitionistic type theory. Bibliopolis Naples (1984)"},{"key":"35_CR13","unstructured":"Morris, P.: Constructing Universes for Generic Programming. Ph.D. thesis, University of Nottingham (2007)"},{"key":"35_CR14","unstructured":"Nordvall Forsberg, F., Setzer, A.: Induction-induction: Agda development and extended version (2010), \n                    \n                      http:\/\/cs.swan.ac.uk\/~csfnf\/induction-induction\/"},{"key":"35_CR15","first-page":"191","volume-title":"Twenty five years of constructive type theory","author":"E. Palmgren","year":"1998","unstructured":"Palmgren, E.: On universes in type theory. In: Sambin, G., Smith, J. (eds.) Twenty five years of constructive type theory, pp. 191\u2013204. Oxford University Press, Oxford (1998)"},{"key":"35_CR16","unstructured":"Streicher, T.: Investigations into intensional type theory. Habilitiation Thesis (1993)"},{"key":"35_CR17","unstructured":"The Agda Team: The Agda wiki (2010), \n                    \n                      http:\/\/wiki.portal.chalmers.se\/agda\/"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15205-4_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T03:02:33Z","timestamp":1606186953000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15205-4_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642152047","9783642152054"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15205-4_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}