{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:30:40Z","timestamp":1761597040292},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540427520"},{"type":"electronic","value":"9783540455042"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45504-3_7","type":"book-chapter","created":{"date-parts":[[2007,8,13]],"date-time":"2007-08-13T22:56:02Z","timestamp":1187045762000},"page":"93-113","source":"Crossref","is-referenced-by-count":19,"title":["Indexed Induction-Recursion"],"prefix":"10.1007","author":[{"given":"Peter","family":"Dybjer","sequence":"first","affiliation":[]},{"given":"Anton","family":"Setzer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,10,2]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"P. Aczel. Frege Structures and the Notions of Proposition, Truth, and Set, pages 31\u201359. North-Holland, 1980.","DOI":"10.1016\/S0049-237X(08)71252-7"},{"key":"7_CR2","unstructured":"T. Altenkirch, V. Gaspes, B. Nordstr\u00f6m, and B. von Sydow. A user\u2019s guide to ALF. http:\/\/www.www.cs.chalmers.se\/ComputingScience\/Research\/ Logic\/alf\/guide.html URL, 1996."},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"A. Bove and V. Capretta. Nested general recursion and partiality in type theory. To appear in the Proceedings of TPHOL 2001.","DOI":"10.1007\/3-540-44755-5_10"},{"key":"7_CR4","unstructured":"C. Coquand. Agda. 2000. http:\/\/www.cs.chalmers.se\/catarina\/agda\/ ."},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"C. Coquand. A realizability interpretation of Martin-L\u00f6f\u2019s type theory. In G. Sambin and J. Smith, editors, Twenty-Five Years of Constructive Type Theory. Oxford University Press, 1998.","DOI":"10.1093\/oso\/9780198501275.003.0007"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"P. Dybjer. Inductive sets and families in Martin-L\u00f6f\u2019s type theory and their settheoretic semantics. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 280\u2013306. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.012"},{"key":"7_CR7","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/BF01211308","volume":"6","author":"P. Dybjer","year":"1994","unstructured":"P. Dybjer. Inductive families. Formal Aspects of Computing, 6:440\u2013465, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"P. Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65(2), June 2000.","DOI":"10.2307\/2586554"},{"key":"7_CR9","series-title":"Lect Notes Comput Sci","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":"P. Dybjer and A. Setzer. A finite axiomatization of inductive-recursive definitions. In J.-Y. Girard, editor, Typed Lambda Calculi and Applications, volume 1581 of Lecture Notes in Computer Science, pages 129\u2013146. Springer, April 1999."},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"P. Dybjer and A. Setzer. Induction-recursion and initial algebras. Submitted for publication, April 2000.","DOI":"10.1007\/3-540-45504-3_7"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"P. Dybjer and A. Setzer. Indexed induction-recursion. To appear as a Report of Institut Mittag-Leffler, 2001.","DOI":"10.1007\/3-540-45504-3_7"},{"key":"7_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/3-540-58085-9_78","volume-title":"Types for proofs and programs","author":"L. Magnusson","year":"1994","unstructured":"L. Magnusson and B. Nordstr\u00f6m. The ALF proof editor and its proof engine. In Types for proofs and programs, volume 806 of Lecture Notes in Computer Science, pages 213\u2013317. Springer, 1994."},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"P. Martin-L\u00f6f. An intuitionistic theory of types: Predicative part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium \u201873, pages 73\u2013118. North-Holland, 1975.","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"P. Martin-L\u00f6f. Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science, VI, 1979, pages 153\u2013175. North-Holland, 1982.","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"7_CR15","unstructured":"P. Martin-L\u00f6f. On the meaning of the logical constants and the justification of the logical laws, 1983. Notes from a series of lectures given in Siena."},{"key":"7_CR16","unstructured":"P. Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, 1984."},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"P. Martin-L\u00f6f. An intuitionistic theory of types. In G. Sambin and J. Smith, editors, Twenty-Five Years of Constructive Type Theory. Oxford University Press, 1998.Reprinted version of an unpublished report from 1972.","DOI":"10.1093\/oso\/9780198501275.003.0010"},{"key":"7_CR18","unstructured":"B. Nordstr\u00f6m, K. Petersson, and J. Smith. Programming in Martin-L\u00f6f\u2019s Type Theory: an Introduction. Oxford University Press, 1990."},{"key":"7_CR19","unstructured":"E. Palmgren. On Fixed Point Operators, Inductive Definitions and Universes in Martin-L\u00f6f\u2019 s Type Theory. PhD thesis, Uppsala University, 1991."},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"E. Palmgren. On universes in type theory. In G. Sambin and J. Smith, editors, Twenty-Five Years of Constructive Type Theory. Oxford University Press, 1998.","DOI":"10.1093\/oso\/9780198501275.003.0012"},{"key":"7_CR21","series-title":"Lect Notes Comput Sci","first-page":"328-245","volume-title":"Proceedings Typed \u03bb-Calculus and Applications","author":"C. Paulin-Mohring","year":"1993","unstructured":"C. Paulin-Mohring. Inductive definitions in the system Coq-rules and properties. In Proceedings Typed \u03bb-Calculus and Applications, pages 328-245. Springer-Verlag, LNCS, March 1993."}],"container-title":["Lecture Notes in Computer Science","Proof Theory in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45504-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,21]],"date-time":"2021-08-21T17:51:24Z","timestamp":1629568284000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45504-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540427520","9783540455042"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-45504-3_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}