{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:04:37Z","timestamp":1767927877177,"version":"3.49.0"},"reference-count":36,"publisher":"Elsevier BV","issue":"1-3","license":[{"start":{"date-parts":[[2003,12,1]],"date-time":"2003-12-01T00:00:00Z","timestamp":1070236800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":3516,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Pure and Applied Logic"],"published-print":{"date-parts":[[2003,12]]},"DOI":"10.1016\/s0168-0072(02)00096-9","type":"journal-article","created":{"date-parts":[[2003,9,3]],"date-time":"2003-09-03T13:20:33Z","timestamp":1062595233000},"page":"1-47","source":"Crossref","is-referenced-by-count":37,"title":["Induction\u2013recursion and initial algebras"],"prefix":"10.1016","volume":"124","author":[{"given":"Peter","family":"Dybjer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anton","family":"Setzer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0168-0072(02)00096-9_BIB1","series-title":"The Kleene Symposium","first-page":"31","article-title":"Frege structures and the notions of proposition, truth, and set","author":"Aczel","year":"1980"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB2","unstructured":"S. Allen, A non-type-theoretic semantics for type-theoretic language, Ph.D. Thesis, Department of Computer Science, Cornell University, 1987."},{"key":"10.1016\/S0168-0072(02)00096-9_BIB3","series-title":"Logic Colloquium \u201990, ASL Summer Meeting Helsinki","first-page":"1","article-title":"A note on the ordinal analysis of KPM","volume":"vol. 2","author":"Buchholz","year":"1993"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB4","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/0168-0072(86)90053-9","article-title":"Generalized algebraic theories and contextual categories","volume":"32","author":"Cartmell","year":"1986","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB5","unstructured":"C. Coquand, The Agda homepage, February 2000. http:\/\/www.cs.chalmers.se\/~catarina\/agda\/."},{"key":"10.1016\/S0168-0072(02)00096-9_BIB6","doi-asserted-by":"crossref","unstructured":"T. Coquand, C. Paulin, Inductively defined types, preliminary version, in: COLOG \u201988, Internat. Conf. on Computer Logic, Lecture Notes Computer Science, vol. 417, Springer, Berlin, 1990.","DOI":"10.1007\/3-540-52335-9_47"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB7","series-title":"Logical Frameworks","first-page":"280","article-title":"Inductive sets and families in Martin-L\u00f6f's type theory and their set-theoretic semantics","author":"Dybjer","year":"1991"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB8","unstructured":"P. Dybjer, Universes and a general notion of simultaneous inductive\u2013recursive definition in type theory, in: B. Nordstr\u00f6m, K. Petersson, G. Plotkin (Eds.), Proceedings of the 1992 Workshop on Types for Proofs and Programs, 1992."},{"key":"10.1016\/S0168-0072(02)00096-9_BIB9","doi-asserted-by":"crossref","first-page":"440","DOI":"10.1007\/BF01211308","article-title":"Inductive families","volume":"6","author":"Dybjer","year":"1994","journal-title":"Formal Aspects Comput."},{"key":"10.1016\/S0168-0072(02)00096-9_BIB10","doi-asserted-by":"crossref","unstructured":"P. Dybjer, Internal type theory, in: TYPES \u201995, Types for Proofs and Programs, Lecture Notes in Computer Science, Springer, Berlin, 1996, pp 120\u2013134.","DOI":"10.1007\/3-540-61780-9_66"},{"issue":"2","key":"10.1016\/S0168-0072(02)00096-9_BIB11","doi-asserted-by":"crossref","first-page":"525","DOI":"10.2307\/2586554","article-title":"A general formulation of simultaneous inductive\u2013recursive definitions in type theory","volume":"65","author":"Dybjer","year":"2000","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB12","series-title":"Typed Lambda Calculi and Applications","first-page":"129","article-title":"A finite axiomatization of inductive\u2013recursive definitions","volume":"vol. 1581","author":"Dybjer","year":"1999"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB13","series-title":"Proof Theory in Computer Science","first-page":"93","article-title":"Indexed induction\u2013recursion","volume":"vol. 2183","author":"Dybjer","year":"2001"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB14","series-title":"Semantics and Logics of Computation","first-page":"79","article-title":"Syntax and semantics of dependent types","author":"Hofmann","year":"1997"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB15","article-title":"Introduction to higher order categorical logic","volume":"vol. 7","author":"Lambek","year":"1986"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB16","unstructured":"C. L\u00f6fwall, G. Sj\u00f6din, Strong normalizability in Martin-L\u00f6f's type theory, Technical Report R91-09, Swedish Institute of Computer Science, 1991."},{"key":"10.1016\/S0168-0072(02)00096-9_BIB17","series-title":"Logic Colloquium \u201873","first-page":"73","article-title":"An intuitionistic theory of types: predicative part","author":"Martin-L\u00f6f","year":"1975"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB18","doi-asserted-by":"crossref","unstructured":"P. Martin-L\u00f6f, Constructive mathematics and computer programming, in: Logic, Methodology and Philosophy of Science, VI, 1979, North-Holland, Amsterdam, 1982, pp. 153\u2013175.","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB19","unstructured":"P. Martin-L\u00f6f, Intuitionistic Type Theory, Bibliopolis, Napoli, 1984."},{"key":"10.1016\/S0168-0072(02)00096-9_BIB20","doi-asserted-by":"crossref","unstructured":"P. Martin-L\u00f6f, An intuitionistic theory of types, in: G. Sambin, J. Smith (Eds.), Twenty-Five Years of Constructive Type Theory, Oxford University Press, 1998, pp. 127\u2013172 (Reprinted version of an unpublished report from 1972).","DOI":"10.1093\/oso\/9780198501275.003.0010"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB21","unstructured":"P.F. Mendler, Predicative type universes and primitive recursion, in: Proc. 6th Annual Symp. on Logic in Computer Science, IEEE Computer Society Press, Silver Spring, MD, 1991."},{"key":"10.1016\/S0168-0072(02)00096-9_BIB22","series-title":"Programming in Martin-L\u00f6f's Type Theory: An Introduction","author":"Nordstr\u00f6m","year":"1990"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB23","unstructured":"E. Palmgren, On fixed point operators, inductive definitions and universes in Martin-L\u00f6f's type theory, Ph.D. Thesis, Uppsala University, 1991."},{"key":"10.1016\/S0168-0072(02)00096-9_BIB24","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/BF01269951","article-title":"Type-theoretic interpretation of iterated, strictly positive inductive definitions","volume":"32","author":"Palmgren","year":"1992","journal-title":"Arch. Math. Logic"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB25","series-title":"Twenty-Five Years of Constructive Type Theory","first-page":"191","article-title":"On universes in type theory","author":"Palmgren","year":"1998"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB26","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring, Inductive definitions in the system Coq\u2014rules and properties, in: Typed lambda calculi and applications, Lecture Notes in Computer Science, vol. 664, Springer, Berlin, 1993, pp. 328\u2013345.","DOI":"10.1007\/BFb0037116"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB27","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/BF01651328","article-title":"Ordinal notations based on a weakly Mahlo cardinal","volume":"29","author":"Rathjen","year":"1990","journal-title":"Arch. Math. Logic"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB28","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1007\/BF01621475","article-title":"Proof-theoretical analysis of KPM","volume":"30","author":"Rathjen","year":"1991","journal-title":"Arch. Math. Logic"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB29","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/BF01275469","article-title":"Collapsing functions based on recursively large cardinals","volume":"33","author":"Rathjen","year":"1994","journal-title":"Arch. Math. Logic"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB30","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/S0168-0072(97)00072-9","article-title":"Inaccessibility in constructive set theory and type theory","volume":"94","author":"Rathjen","year":"1998","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB31","doi-asserted-by":"crossref","unstructured":"D.S. Scott, Constructive validity, in: Symp. on Automatic Demonstration, Lecture Notes in Mathematics, vol. 125, Springer, Berlin, 1970, pp. 237\u2013275.","DOI":"10.1007\/BFb0060636"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB32","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1017\/S0305004100061284","article-title":"Locally cartesian closed categories and type theory","volume":"95","author":"Seely","year":"1984","journal-title":"Proc. Cambridge Philos. Soc."},{"key":"10.1016\/S0168-0072(02)00096-9_BIB33","unstructured":"A. Setzer, Proof theoretical strength of Martin-L\u00f6f type theory with W-type and one universe, Ph.D. Thesis, Fakult\u00e4t f\u00fcr Mathematik der Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen, 1993."},{"key":"10.1016\/S0168-0072(02)00096-9_BIB34","unstructured":"A. Setzer, A model for a type theory with Mahlo universe, Draft, available from http:\/\/www-compsci.swan.ac.uk\/~csetzer\/, 1996."},{"key":"10.1016\/S0168-0072(02)00096-9_BIB35","first-page":"128","article-title":"A type theory for Mahlo universes, Abstract for Logic Colloquium 95","volume":"3","author":"Setzer","year":"1997","journal-title":"Bull. Symbolic Logic"},{"key":"10.1016\/S0168-0072(02)00096-9_BIB36","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/s001530050140","article-title":"Extending Martin-L\u00f6f type theory by one Mahlo-universe","volume":"39","author":"Setzer","year":"2000","journal-title":"Arch. Math. Logic"}],"container-title":["Annals of Pure and Applied Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007202000969?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007202000969?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2021,6,10]],"date-time":"2021-06-10T12:58:41Z","timestamp":1623329921000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0168007202000969"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,12]]},"references-count":36,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2003,12]]}},"alternative-id":["S0168007202000969"],"URL":"https:\/\/doi.org\/10.1016\/s0168-0072(02)00096-9","relation":{},"ISSN":["0168-0072"],"issn-type":[{"value":"0168-0072","type":"print"}],"subject":[],"published":{"date-parts":[[2003,12]]}}}