{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T14:27:01Z","timestamp":1725460021100},"publisher-location":"Berlin\/Heidelberg","reference-count":8,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540582770"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0049338","type":"book-chapter","created":{"date-parts":[[2006,3,6]],"date-time":"2006-03-06T18:58:16Z","timestamp":1141671496000},"page":"295-304","source":"Crossref","is-referenced-by-count":4,"title":["Normalization for typed lambda calculi with explicit substitution"],"prefix":"10.1007","author":[{"given":"Eike","family":"Ritter","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"19_CR1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. L\u00e9vy. Explicit substitutions. Journal of Functional Programming, 1(4):375\u2013416, 1991.","journal-title":"Journal of Functional Programming"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"P.-L. Curien, T. Hardin, and A. R\u00edos. Strong normalisation of substitutions. In I.M. Havel and V. Koubek, editors, Mathematical Foundations of Computer Science 1992, pages 209\u2013217. Lecture Notes in Computer Science No. 629, Berlin, Heidelberg, New York, 1992.","DOI":"10.1007\/3-540-55808-X_19"},{"key":"19_CR3","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N.G. Bruijn De","year":"1972","unstructured":"N.G. De Bruijn. Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation. Indag. Math, 34:381\u2013392, 1972.","journal-title":"Indag. Math"},{"key":"19_CR4","volume-title":"Proofs and Types","author":"J. Girard","year":"1989","unstructured":"Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and Types. Cambridge University Press, Cambridge, 1989."},{"key":"19_CR5","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/0304-3975(86)90035-6","volume":"46","author":"T. Hardin","year":"1986","unstructured":"Th\u00e9r\u00e8se Hardin and Alain Laville. Proof of termination of the rewriting system Subst on CCL. Theoretical Computer Science, 46:305\u2013312, 1986.","journal-title":"Theoretical Computer Science"},{"key":"19_CR6","unstructured":"Gy\u00f6rgy E. R\u00e9v\u00e9sz. Lambda-calculus, combinators and functional programming. Number 4 in Cambridge tracts in theoretical computer science. Cambridge University Press, 1988."},{"key":"19_CR7","unstructured":"Eike Ritter. Categorical Abstract Machines for Higher-Order Lambda Calculi.PhD thesis, University of Cambridge, 1992. Also available as Technical Report No. 297."},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"W. W. Tait. A realizability interpretation of the theory of species. In R. Parikh, editor, Logic Colloquium, pages 240\u2013251. LNM 453, Springer Verlag, 1975.","DOI":"10.1007\/BFb0064875"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0049338.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:55:46Z","timestamp":1607550946000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0049338"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540582770"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/bfb0049338","relation":{},"subject":[]}}