{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T14:15:31Z","timestamp":1725459331615},"publisher-location":"Berlin\/Heidelberg","reference-count":7,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540565175"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0037120","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T15:21:36Z","timestamp":1138202496000},"page":"391-405","source":"Crossref","is-referenced-by-count":3,"title":["Lower and upper bounds for reductions of types in \u03bb and \u03bbP (extended abstract)"],"prefix":"10.1007","author":[{"given":"Jan","family":"Springintveld","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Barendregt, H.P., \u2018Lambda calculi with types', in: Abramski, S., Gabbay, D.M. & Maibaum, T.S.E., eds., Handbook of Logic in Computer Science, Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"27_CR2","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, Th. and Huet, G., \u2018The calculus of constructions', Information and Computation, Vol. 76, pp. 95\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"27_CR3","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"Geuvers, H. and Nederhof, M.-J., \u2018Modular proof of strong normalization for the calculus of constructions', in: The Journal of Functional Programming, Vol.1, pp. 155\u2013189, 1991.","journal-title":"The Journal of Functional Programming"},{"key":"27_CR4","unstructured":"Pollack, R., \u2018Typechecking in pure type systems', in: N\u00f6rdstrom, B., Petersson, K. and Plotkin, G., eds., Proceedings of the 1992 Workshop on Types for Proofs and Programs, B\u00e5stad, June 92, pp. 289\u2013306."},{"key":"27_CR5","volume-title":"Subrecursion. Functions and Hierarchies","author":"H.E. Rose","year":"1984","unstructured":"Rose, H.E., Subrecursion. Functions and Hierarchies, Clarendon Press, Oxford, 1984."},{"key":"27_CR6","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/BF01621476","volume":"30","author":"H. Schwichtenberg","year":"1991","unstructured":"Schwichtenberg, H., \u2018An upperbound for reduction sequences in the typed \u03bb-calculus', Archive for Mathematical Logic, Vol.30, pp. 405\u2013408, 1991.","journal-title":"Archive for Mathematical Logic"},{"key":"27_CR7","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(79)90007-0","volume":"9","author":"R. Statman","year":"1979","unstructured":"Statman, R., \u2018The typed lambda calculus is not elementary recursive', Theoretical Computer Science, Vol. 9, pp. 73\u201381, 1979.","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0037120.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,2]],"date-time":"2024-02-02T14:04:08Z","timestamp":1706882648000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0037120"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540565175"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/bfb0037120","relation":{},"subject":[]}}