{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T14:07:37Z","timestamp":1751983657703},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540415176"},{"type":"electronic","value":"9783540445579"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44557-9_2","type":"book-chapter","created":{"date-parts":[[2007,5,31]],"date-time":"2007-05-31T23:04:24Z","timestamp":1180652664000},"page":"21-40","source":"Crossref","is-referenced-by-count":6,"title":["A Predicative Strong Normalisation Proof for a \u03bbCalculus with Interleaving Inductive Types"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Abel","sequence":"first","affiliation":[]},{"given":"Thorsten","family":"Altenkirch","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,6,11]]},"reference":[{"unstructured":"Andreas Abel and Thorsten Altenkirch. A predicative analysis of structural recursion. Submitted to the Journal of Functional Programming, December 1999.","key":"2_CR1"},{"key":"2_CR2","volume-title":"A semantic analysis of structural recursion","author":"A. Abel","year":"1999","unstructured":"Andreas Abel. A semantic analysis of structural recursion. Master\u2019s thesis, Ludwig-Maximilians-University Munich, 1999. http:\/\/www.informatik.uni-muenchen.de\/~abel\/publications\/ ."},{"unstructured":"Peter Aczel. Notes on constructive set theory. Available from the WWW, 1997.","key":"2_CR3"},{"unstructured":"Thorsten Altenkirch. Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinburgh, November 1993.","key":"2_CR4"},{"doi-asserted-by":"crossref","unstructured":"Thorsten Altenkirch. Logical relations and inductive\/coinductive types. 1998.","key":"2_CR5","DOI":"10.1007\/10703163_23"},{"doi-asserted-by":"crossref","unstructured":"Thorsten Altenkirch and Bernhard Reus. Monadic presentations of lambda terms using generalized inductive types. In Computer Science Logic 99, 1999.","key":"2_CR6","DOI":"10.1007\/3-540-48168-0_32"},{"key":"2_CR7","volume-title":"Starke Normalisierung f\u00fcr die Heyting-Arithmetik mit induktiven Typen","author":"H. Benl","year":"1998","unstructured":"Holger Benl. Starke Normalisierung f\u00fcr die Heyting-Arithmetik mit induktiven Typen. Master\u2019s thesis, Ludwig-Maximillians-Universit\u00e4t, M\u00fcnchen, 1998."},{"unstructured":"Fr\u00e9d\u00e9ric Blanqui, Jean-Pierre Jouannaud, and Mitsuhiro Okada. Inductive data type systems. To appear in Theoretical Computer Science, 1999.","key":"2_CR8"},{"doi-asserted-by":"crossref","unstructured":"Wilfried Buchholz. The \u03bb\u03bc+1-rule. In Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, volume 897 of Lecture Notes in Mathematics, pages 188\u2013233. 1981.","key":"2_CR9","DOI":"10.1007\/BFb0091898"},{"key":"2_CR10","series-title":"Lect Notes Comput Sci","first-page":"50","volume-title":"Lecture Notes in Computer Science","author":"T. Coquand","year":"1989","unstructured":"Thierry Coquand and Christine Mohring. Inductively defined types. In P. L\u00f6f and G. Mints, editors, LNCS 389, volume 417 of Lecture Notes in Computer Science, pages 50\u201366. Springer-Verlag, 1989."},{"doi-asserted-by":"crossref","unstructured":"Peter Dybjer. Inductive sets and families in Martin-L\u00f6f\u2019s type theory and their set-theoretic semantics. Technical Report Report 62, Programming Methodology Group, Chalmers University, 1991.","key":"2_CR11","DOI":"10.1017\/CBO9780511569807.012"},{"unstructured":"Herman Geuvers. Inductive and coinductive types with iteration and recursion. In Workshop on Types for Proofs and Programs, B\u00e5astad, pages 193\u2013217, 1992.","key":"2_CR12"},{"unstructured":"J. Y. Girard. Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dans l\u2019arith\u00e9tique d\u2019ordre sup\u00e9rieur. PhD thesis, Universit\u00e9 Paris VII, 1972.","key":"2_CR13"},{"unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989.","key":"2_CR14"},{"unstructured":"Tatsuya Hagino. A Categorical Programming Language. PhD thesis, University of Edinburgh, September 1987.","key":"2_CR15"},{"issue":"6","key":"2_CR16","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1017\/S0956796898003128","volume":"8","author":"C.B. Jay","year":"1998","unstructured":"C.B. Jay, G. Bell\u00e8, and E. Moggi. Functorial ML. Journal of Functional Programming, 8(6):573\u2013619, 1998.","journal-title":"Journal of Functional Programming"},{"doi-asserted-by":"crossref","unstructured":"J. P. Jouannaud and M. Okada. Abstract data type systems. Theoretical Computer Science, 173, 1997.","key":"2_CR17","DOI":"10.1016\/S0304-3975(96)00161-2"},{"key":"2_CR18","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/S0168-0072(96)00021-8","volume":"84","author":"R. Loader","year":"1997","unstructured":"Ralph Loader. Equational theories for inductive types. Annals of Pure and Applied Logic, 84:175\u2013217, 1997.","journal-title":"Annals of Pure and Applied Logic"},{"unstructured":"Zhaohui Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990.","key":"2_CR19"},{"unstructured":"Per Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, 1984.","key":"2_CR20"},{"unstructured":"Ralph Matthes. Extensions of System F by Iteration And Primitive Recursion on Monotone Inductive Types. PhD thesis, University of Munich, 1998.","key":"2_CR21"},{"unstructured":"Nax P. Mendler. Inductive Definition in Type Theory. PhD thesis, Cornell University, 1988.","key":"2_CR22"},{"key":"2_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-13346-1_7","volume-title":"Semantics of Data Types","author":"J. C. Reynolds","year":"1984","unstructured":"John C. Reynolds. Polymorphism is not set-theoretic. In Gilles Kahn, David B. MacQueen, and Gordon D. Plotkin, editors, Semantics of Data Types, volume 173 of Lecture Notes in Computer Science, pages 145\u2013156, Berlin, 1984. Springer-Verlag."},{"issue":"2","key":"2_CR24","doi-asserted-by":"publisher","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W. W. Tait","year":"1967","unstructured":"W. W. Tait. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic, 32(2):198\u2013212, June 1967.","journal-title":"Journal of Symbolic Logic"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44557-9_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,22]],"date-time":"2020-04-22T12:22:36Z","timestamp":1587558156000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44557-9_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540415176","9783540445579"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-44557-9_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}