{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:09:48Z","timestamp":1725664188798},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540612544"},{"type":"electronic","value":"9783540683896"}],"license":[{"start":{"date-parts":[[1996,1,1]],"date-time":"1996-01-01T00:00:00Z","timestamp":820454400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61254-8_27","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:20:06Z","timestamp":1330273206000},"page":"201-220","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Two different strong normalization proofs?"],"prefix":"10.1007","author":[{"given":"Jaco","family":"van de Pol","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"12_CR1","first-page":"91","volume-title":"volume 664 of LNCS","author":"U. Berger","year":"1993","unstructured":"U. Berger. Program extraction from normalization proofs. In M. Bezem and J.F. Groote ed., Proc. of TLCA '93, Utrecht, volume 664 of LNCS, pages 91\u2013106. Springer Verlag, 1993."},{"key":"12_CR2","first-page":"457","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"R.O. Gandy","year":"1980","unstructured":"R.O. Gandy. Proofs of strong normalization. In J.R. Hindley and J.P. Seidin ed., To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 457\u2013477. Academic Press, London, 1980."},{"key":"12_CR3","unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types, volume 7 of Cambridge tracts in theoretical computer science. Cambridge University Press, 1989."},{"key":"12_CR4","unstructured":"G. Kreisel. Interpretation of analysis by means of constructive functionals of finite types. In A. Heyting ed., Constructivity in Mathematics, pages 101\u2013128. North-Holland, 1959."},{"key":"12_CR5","unstructured":"R. Loader. Normalisation by translation. http:\/\/sable.ox.ac.uk\/ loader\/, 1995."},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"J.C. van de Pol. Termination proofs for higher-order rewrite systems. In J. Heering et al ed., Proc. of HOA '93, volume 816 of LNCS, pages 305\u2013325. Springer Verlag, 1994.","DOI":"10.1007\/3-540-58233-9_14"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"J.C. van de Pol and H. Schwichtenberg. Strict functionals for termination proofs. In M. Dezani-Ciancaglini and G. Plotkin ed., Proc. of TLCA'95, volume 902 of LNCS, pages 350\u2013364. Springer Verlag, 1995.","DOI":"10.1007\/BFb0014064"},{"key":"12_CR8","first-page":"235","volume-title":"Ideas and results in proof theory","author":"D. Prawitz","year":"1971","unstructured":"D. Prawitz. Ideas and results in proof theory. In J.E. Fenstad ed., Proc. of the 2nd Scandinavian Logic Symposium, pages 235\u2013307, Amsterdam, 1971. North-Holland."},{"key":"12_CR9","first-page":"198","volume":"32","author":"W.W. Tait","year":"1967","unstructured":"W.W. Tait. Intensional interpretation of functionals of finite types I. JSL, 32:198\u2013212, 1967.","journal-title":"JSL"},{"key":"12_CR10","volume-title":"Number 344 in LNM","author":"A.S. Troelstra","year":"1973","unstructured":"A.S. Troelstra. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Number 344 in LNM. Springer Verlag, Berlin, 1973. A 2nd corrected edition appeared as ILLC X-93-05, University of Amsterdam."},{"issue":"4","key":"12_CR11","first-page":"479","volume":"90","author":"R. Vrijer de","year":"1987","unstructured":"R. de Vrijer. Exactly estimating functionals and strong normalization. Proc. of the Koninklijke Nederlandse Akademie van Wetenschappen, 90(4):479\u2013493, Dec 1987.","journal-title":"Proc. of the Koninklijke Nederlandse Akademie van Wetenschappen"}],"container-title":["Lecture Notes in Computer Science","Higher-Order Algebra, Logic, and Term Rewriting"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61254-8_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T18:15:54Z","timestamp":1578507354000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61254-8_27"}},"subtitle":["Computability versus functional of finite type"],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540612544","9783540683896"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-61254-8_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]},"assertion":[{"value":"1 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}