{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:05:47Z","timestamp":1725566747804},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540282310"},{"type":"electronic","value":"9783540318972"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11538363_4","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T13:35:33Z","timestamp":1127828133000},"page":"27-35","source":"Crossref","is-referenced-by-count":0,"title":["An Abstract Strong Normalization Theorem"],"prefix":"10.1007","author":[{"given":"Ulrich","family":"Berger","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","volume":"5","author":"G. Plotkin","year":"1977","unstructured":"Plotkin, G.: LCF considered as a programming language. Theoretical Computer Science\u00a05, 223\u2013255 (1977)","journal-title":"Theoretical Computer Science"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/11494645_4","volume-title":"New Computational Paradigms","author":"U. Berger","year":"2005","unstructured":"Berger, U.: Continuous semantics for strong normalization. In: Cooper, S.B., L\u00f6we, B., Torenvliet, L. (eds.) CiE 2005. LNCS, vol.\u00a03526, pp. 23\u201334. Springer, Heidelberg (2005)"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Berger, U.: Strong normalization for applied lambda calculi. Submitted to: Logical Methods in Computer Science, January 2005 (2005)","DOI":"10.2168\/LMCS-1(2:3)2005"},{"key":"4_CR4","first-page":"1","volume-title":"Recursive Function Theory: Proc. Symposia in Pure Mathematics","author":"C. Spector","year":"1962","unstructured":"Spector, C.: Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics. In: Dekker, F.D.E. (ed.) Recursive Function Theory: Proc. Symposia in Pure Mathematics, vol.\u00a05, pp. 1\u201327. American Mathematical Society, Providence (1962)"},{"key":"4_CR5","first-page":"107","volume":"20","author":"W.A. Howard","year":"1968","unstructured":"Howard, W.A.: Functional interpretation of bar induction by bar recursion. Composito Mathematicae\u00a020, 107\u2013124 (1968)","journal-title":"Composito Mathematicae"},{"key":"4_CR6","doi-asserted-by":"publisher","first-page":"600","DOI":"10.2307\/2586854","volume":"63","author":"S. Berardi","year":"1998","unstructured":"Berardi, S., Bezem, M., Coquand, T.: On the computational content of the axiom of choice. Journal of Symbolic Logic\u00a063, 600\u2013622 (1998)","journal-title":"Journal of Symbolic Logic"},{"key":"4_CR7","volume-title":"Logic Colloquium 2001","author":"U. Berger","year":"2005","unstructured":"Berger, U., Oliva, P.: Modified bar recursion and classical dependent choice. In: Logic Colloquium 2001, Springer, Heidelberg (2005)"},{"key":"4_CR8","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1109\/LICS.2004.1319627","volume-title":"Proceedings of the Ninetenth Annual IEEE Symposium on Logic in Computer Science","author":"U. Berger","year":"2004","unstructured":"Berger, U.: A computational interpretation of open induction. In: Titsworth, F. (ed.) Proceedings of the Ninetenth Annual IEEE Symposium on Logic in Computer Science, pp. 326\u2013334. IEEE Computer Society, Los Alamitos (2004)"},{"key":"4_CR9","unstructured":"Scott, D.S.: Outline of a mathematical theory of computation. In: 4th Annual Princeton Conference on Information Sciences and Systems, pp. 169\u2013176 (1970)"},{"key":"4_CR10","volume-title":"Mathematical theory of domains","author":"E. Griffor","year":"1993","unstructured":"Griffor, E., Lindstr\u00f6m, I., Stoltenberg-Hansen, V.: Mathematical theory of domains. Cambridge University Press, Cambridge (1993)"},{"key":"4_CR11","first-page":"1","volume-title":"Handbook of Logic in Computer Science","author":"S. Abramsky","year":"1994","unstructured":"Abramsky, S., Jung, A.: Domain theory. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol.\u00a03, pp. 1\u2013168. Clarendon Press, Oxford (1994)"},{"key":"4_CR12","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/0020-0190(88)90126-3","volume":"29","author":"J.C. Raoult","year":"1988","unstructured":"Raoult, J.C.: Proving open properties by induction. Information processing letters\u00a029, 19\u201323 (1988)","journal-title":"Information processing letters"},{"key":"4_CR13","unstructured":"Coquand, T.: A note on the open induction principle (1997)"},{"key":"4_CR14","unstructured":"Mahboubi, A.: An induction principle over real numbers. Submitted to Archive for Mathematical Logic (2004)"},{"key":"4_CR15","doi-asserted-by":"publisher","first-page":"833","DOI":"10.1017\/S0305004100003844","volume":"59","author":"C. Nash-Williams","year":"1963","unstructured":"Nash-Williams, C.: On well-quasi-ordering finite trees. Proc. Cambridge Phil. Soc.\u00a059, 833\u2013835 (1963)","journal-title":"Proc. Cambridge Phil. Soc."},{"key":"4_CR16","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1016\/S0049-237X(08)70853-X","volume-title":"Proceedings of the Second Scandinavian Logic Symposium","author":"W. Tait","year":"1971","unstructured":"Tait, W.: Normal form theorem for barrecursive functions of finite type. In: Fenstad, J. (ed.) Proceedings of the Second Scandinavian Logic Symposium, pp. 353\u2013367. North\u2013Holland, Amsterdam (1971)"},{"key":"4_CR17","unstructured":"Girard, J.Y.: Interpr\u00e9tation functionelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. PhD thesis, Universit\u00e9 Paris VII (1972)"},{"key":"4_CR18","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/BF02007566","volume":"25","author":"M. Bezem","year":"1985","unstructured":"Bezem, M.: Strong normalization of barrecursive terms without using infinite terms. Archive for Mathematical Logic\u00a025, 175\u2013181 (1985)","journal-title":"Archive for Mathematical Logic"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/BFb0049336","volume-title":"Computer Science Logic","author":"L. Ong","year":"1994","unstructured":"Ong, L., Ritter, E.: A generic normalisation argument: Application to the calculus of constructions. In: Meinke, K., B\u00f6rger, E., Gurevich, Y. (eds.) CSL 1993. LNCS, vol.\u00a0832, pp. 261\u2013279. Springer, Heidelberg (1994)"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/BFb0037106","volume-title":"Typed Lambda Calculi and Applications","author":"J. Hyland","year":"1993","unstructured":"Hyland, J., Ong, C.H.: Modified realizability semantics and strong normalization proofs. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 179\u2013194. Springer, Heidelberg (1993)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11538363_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:54:20Z","timestamp":1619506460000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11538363_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540282310","9783540318972"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/11538363_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}