{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:26:36Z","timestamp":1725456396055},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540645702"},{"type":"electronic","value":"9783540693536"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0028014","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T07:02:06Z","timestamp":1132642926000},"page":"177-188","source":"Crossref","is-referenced-by-count":2,"title":["A proof-theoretical investigation of Zantema's problem"],"prefix":"10.1007","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]},{"given":"Henrik","family":"Persson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,15]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"P. Aczel. An Introduction to Inductive Definitions. In J. Barwise, editor, Handbook of Mathematical Logic, pages 739\u2013782. North-Holland Publishing Company, 1977.","DOI":"10.1016\/S0049-237X(08)71120-0"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Th. Coquand. Constructive topology and combinatorics. In proceeding of the conference Constructivity in Computer Science, San Antonio, LNCS 613, pages 28\u201332, 1992.","DOI":"10.1007\/BFb0021089"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and C. Hoot. Topics in termination. In proceeding of the 5th Conf. Rewriting Techniques and Applications, Montreal, LNCS 690, pages 198\u2013212, 1993.","DOI":"10.1007\/3-540-56868-9_16"},{"issue":"2","key":"11_CR4","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/0304-3975(94)00275-4","volume":"142","author":"N. Dershowitz","year":"1995","unstructured":"N. Dershowitz and C. Hoot. Natural termination. Theoret. Comput. Sci., 142(2):179\u2013207, 1995. Selected papers of the Fifth International Conference on Rewriting Techniques and Applications (Montreal, PQ, 1993).","journal-title":"Theoret. Comput. Sci."},{"key":"11_CR5","unstructured":"H. Lombardi. Relecture constructive de la theorie d'Artin-Schrier. Prepublication, March 1994."},{"key":"11_CR6","unstructured":"C. Murthy. Extracting Constructive Content from Classical Proofs. PhD thesis, Cornell University, 1990."},{"key":"11_CR7","doi-asserted-by":"crossref","first-page":"833","DOI":"10.1017\/S0305004100003844","volume":"59","author":"C. Nash-Williams","year":"1963","unstructured":"C. Nash-Williams. On well-quasi-ordering finite trees. Proceedings of the Cambridge Philosophical Society, 59:833\u2013835, 1963.","journal-title":"Proceedings of the Cambridge Philosophical Society"},{"key":"11_CR8","unstructured":"B. Nordstr\u00f6m, K. Petersson, and J. M. Smith. Programming in Martin-L\u00f6f's Type Theory. An Introduction. Oxford University Press, 1990."},{"key":"11_CR9","doi-asserted-by":"crossref","first-page":"459","DOI":"10.1016\/S0049-237X(08)70771-7","volume-title":"Intuitionism and Proof Theory (Proc. Conf., Buffalo, N. Y., 1968)","author":"C. Parsons","year":"1970","unstructured":"C. Parsons. On a number theoretic choice schema and its relation to induction. In Intuitionism and Proof Theory (Proc. Conf., Buffalo, N. Y., 1968), pages 459\u2013473. North-Holland, Amsterdam, 1970."},{"key":"11_CR10","unstructured":"J. Peterson and K. Hammond. The Haskell 1.3 Report. Technical Report YALEU\/DCS\/RR-1106, Yale University, 1996."},{"key":"11_CR11","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/0020-0190(88)90126-3","volume":"29","author":"J-C. Raoult","year":"1988","unstructured":"J-C. Raoult. Proving open properties by induction. Information processing letters, 29:19\u201323, 1988.","journal-title":"Information processing letters"},{"issue":"2","key":"11_CR12","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1017\/S0022481200028309","volume":"53","author":"S. G. Simpson","year":"1988","unstructured":"S. G. Simpson. Partial realizations of Hilbert's Program. J. Symbolic Logic, 53(2):349\u2013363, 1988.","journal-title":"J. Symbolic Logic"},{"key":"11_CR13","unstructured":"E. Tahhan-Bittar. Non-erasing, right-linear orthogonal term rewrite systems, application to Zantema's problem. Technical Report RR2202, INRIA, France, 1994."},{"key":"11_CR14","unstructured":"W. Pohlers W. Sieg W. Buchholz, S. Feferman. Iterated inductive definitions and subsystems of analysis, volume Recent Proof-Theoretical Studies of Lecture Notes in Mathematics 897 Springer-Verlag, 1981."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028014","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T02:51:36Z","timestamp":1586573496000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028014"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540645702","9783540693536"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0028014","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}