{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T04:12:31Z","timestamp":1748751151750,"version":"3.41.0"},"publisher-location":"Cham","reference-count":12,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319276823"},{"type":"electronic","value":"9783319276830"}],"license":[{"start":{"date-parts":[[2015,12,10]],"date-time":"2015-12-10T00:00:00Z","timestamp":1449705600000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-27683-0_27","type":"book-chapter","created":{"date-parts":[[2015,12,9]],"date-time":"2015-12-09T21:16:29Z","timestamp":1449695789000},"page":"392-406","source":"Crossref","is-referenced-by-count":0,"title":["Levy Labels and Recursive Types"],"prefix":"10.1007","author":[{"given":"Rick","family":"Statman","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,12,10]]},"reference":[{"key":"27_CR1","unstructured":"Barendregt, H.: The Lambda Calculus, Amsterdam (1981)"},{"key":"27_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139032636","volume-title":"Lambda Calculus with Types","author":"H Barendregt","year":"2013","unstructured":"Barendregt, H., Dekkers, J., Statman, R.: Lambda Calculus with Types. Cambridge University Press, Cambridge (2013)"},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"De Vrijer, R.: Extending the lambda calculus with surjective pairing is conservative. In: LICS, pp. 204\u2013215 (1989)","DOI":"10.1109\/LICS.1989.39175"},{"key":"27_CR4","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1090\/S0002-9947-1978-0489603-9","volume":"240","author":"R Hindley","year":"1978","unstructured":"Hindley, R.: Reductions of residuals are finite. Trans. A.M.S 240, 345\u2013361 (1978)","journal-title":"Trans. A.M.S"},{"key":"27_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BFb0029523","volume-title":"Lambda Calculus and Computer Science Theory","author":"JJ Levy","year":"1975","unstructured":"Levy, J.J.: An algebraic interpretation of the lambda beta $$K$$ calculus and a labeled lambda calculus. In: Bohm, C. (ed.) Lambda Calculus and Computer Science Theory. LNCS, vol. 37, pp. 147\u2013165. Springer, Heidelberg (1975)"},{"key":"27_CR6","unstructured":"Klop, J.W.: Combinatory Reduction Sytems. Dissertation: University of Utrecht (1980)"},{"issue":"1","key":"27_CR7","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: Machine oriented logic based on the resolution principle. JACM 12(1), 23\u201341 (1965)","journal-title":"JACM"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/BFb0029537","volume-title":"Lambda Calculus and Computer Science Theory","author":"D Scott","year":"1975","unstructured":"Scott, D.: Some philosophical issues concerning theories of combinators. In: Bohm, C. (ed.) Lambda Calculus and Computer Science Theory. LNCS, vol. 37, pp. 346\u2013366. Springer, Berlin (1975)"},{"key":"27_CR9","unstructured":"Statman, R.: Recursive types and the subject reduction theorem, Technical report 94\u2013164, Deparment of Mathematical Sciences, Carnegie Mellon University (1994)"},{"key":"27_CR10","unstructured":"Statman, R.: Surjective pairing revisited. In: Van Oostrom, V., Van Raamsdonk, F., (eds.), Liber Amicorum for Roel De Vrijer, University of Amsterdam (2009)"},{"key":"27_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-642-20920-8_24","volume-title":"Logic, Language, Information and Computation","author":"R Statman","year":"2011","unstructured":"Statman, R.: On polymorphic types of untyped terms. In: Beklemishev, L.D., Queiroz, R. (eds.) WoLLIC 2011. LNCS, vol. 6642, pp. 239\u2013256. Springer, Heidelberg (2011)"},{"issue":"2:1","key":"27_CR12","first-page":"1","volume":"2","author":"S Stovring","year":"2006","unstructured":"Stovring, S.: Extending the extensional lambda calculus with surjective pairing. Log. Methods Comput. Sci. 2(2:1), 1\u201314 (2006)","journal-title":"Log. Methods Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-27683-0_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T18:39:37Z","timestamp":1748716777000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-27683-0_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,10]]},"ISBN":["9783319276823","9783319276830"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-27683-0_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015,12,10]]}}}