{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:19:56Z","timestamp":1725664796152},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540614647"},{"type":"electronic","value":"9783540685968"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61464-8_51","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:39:43Z","timestamp":1330292383000},"page":"169-183","source":"Crossref","is-referenced-by-count":10,"title":["Combinatory reduction systems with explicit substitution that preserve strong normalisation"],"prefix":"10.1007","author":[{"given":"Roel","family":"Bloo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kristoffer H.","family":"Rose","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"issue":"4","key":"14_CR1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L. and L\u00e9vy, J.-J. (1991). Explicit substitutions. Journal of Functional Programming 1(4): 375\u2013416.","journal-title":"Journal of Functional Programming"},{"key":"14_CR2","unstructured":"Aczel, P. (1978). A general Church-Rosser theorem. Technical report. Univ. of Manchester."},{"key":"14_CR3","first-page":"416","volume-title":"Cyclic lambda graph rewriting","author":"Z. M. Ariola","year":"1994","unstructured":"Ariola, Z. M. and Klop, J. W. (1994). Cyclic lambda graph rewriting. Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press. Paris, France. pp. 416\u2013425. full version forthcoming (Ariola and Klop 1995)."},{"key":"14_CR4","unstructured":"Ariola, Z. M. and Klop, J. W. (1995). Lambda calculus with explicit recursion. Personal Communication."},{"key":"14_CR5","unstructured":"Barendregt, H. P. (1984). The Lambda Calculus: Its Syntax and Semantics. Revised edn. North-Holland."},{"key":"14_CR6","unstructured":"Bloo, R. and Rose, K. H. (1995). Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection. CSN '95 \u2014Computer Science in the Netherlands. pp. 62\u201372. \u2329url: ftp:\/\/ftp.diku.dk\/diku\/semantics\/papers\/ D-246.ps\u232a"},{"key":"14_CR7","first-page":"381","volume":"75","author":"N. G. Bruijn de","year":"1972","unstructured":"de Bruijn, N. G. (1972). Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation with application to the Church-Rosser theorem. Koninklijke Nederlandse Akademie van Wetenschappen, Series A, Mathematical Sciences 75: 381\u2013392. Also chapter C.2 of (Nederpelt, Geuvers and de Vrijer 1994).","journal-title":"Koninklijke Nederlandse Akademie van Wetenschappen, Series A, Mathematical Sciences"},{"key":"14_CR8","volume-title":"UW TR CS-93-44","author":"D. Duggan","year":"1993","unstructured":"Duggan, D. (1993). Higher-order substitution. UW TR CS-93-44. Dept. of Computer Science, University of Waterloo. Waterloo, Ontario, Canada N2L 3G1. \u2329Url: http:\/\/nuada.uwaterloo.ca\/dduggan\/papers\/\u2273"},{"key":"14_CR9","unstructured":"Klop, J. W. (1980). Combinatory Reduction Systems. PhD thesis. University of Utrecht. Also available as Mathematical Centre Tracts 127."},{"key":"14_CR10","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","volume":"121","author":"J. W. Klop","year":"1993","unstructured":"Klop, J. W., van Oostrom, V. and van Raamsdonk, F. (1993). Combinatory reduction systems: Introduction and survey. Theoretical Computer Science 121: 279\u2013308.","journal-title":"Theoretical Computer Science"},{"key":"14_CR11","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1093\/comjnl\/6.4.308","volume":"6","author":"P. J. Landin","year":"1964","unstructured":"Landin, P. J. (1964). The mechanical evaluation of expressions. Computer Journal 6: 308\u2013320.","journal-title":"Computer Journal"},{"key":"14_CR12","first-page":"328","volume-title":"LNCS","author":"P.-A. Melli\u00e8s","year":"1995","unstructured":"Melli\u00e8s, P.-A. (1995). Typed \u03bb-calculi with explicit substitution may not terminate. In Dezani, M. (ed.), Int. Conf. on Typed Lambda Calculus and Applications. LNCS. U of Edinburgh. Springer-Verlag. Edinburgh, Scotland. pp. 328\u2013334."},{"key":"14_CR13","unstructured":"Nederpelt, R. P., Geuvers, J. H. and de Vrijer, R. C. (eds) (1994). Selected Papers on Automath. Vol. 133 of Studies in Logic. North-Holland."},{"key":"14_CR14","first-page":"342","volume-title":"Higher-order critical pairs","author":"T. Nipkow","year":"1991","unstructured":"Nipkow, T. (1991). Higher-order critical pairs. Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press. Amsterdam, The Netherlands. pp. 342\u2013349."},{"key":"14_CR15","first-page":"36","volume-title":"Number 656 in LNCS","author":"K. H. Rose","year":"1992","unstructured":"Rose, K. H. (1992). Explicit cyclic substitutions. In Rusinowitch, M. and R\u00e9my, J.-L. (eds), CTRS '92-3rd International Workshop on Conditional Term Rewriting Systems. Number 656 in LNCS. Springer-Verlag. Pont-a-Mousson, France. pp. 36\u201350. \u2329Url: ftp:\/\/ftp.diku.dk\/diku\/semantics\/papers\/D-143.ps\u232a"},{"key":"14_CR16","series-title":"DIKU report 96\/1","volume-title":"PhD thesis","author":"K. H. Rose","year":"1996","unstructured":"Rose, K. H. (1996). Operational Reduction Models for Functional Programming Languages. PhD thesis. DIKU (University of Copenhagen). Universitetsparken 1, DK-2100 K\u00f8benhavn \u00d8. DIKU report 96\/1."},{"key":"14_CR17","unstructured":"van Oostrom, V. and van Raamsdonk, F. (1995). Weak orthogonality implies confluence: the higher-order case. Technical Report CS-R9501. CWI."}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61464-8_51.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:32:10Z","timestamp":1619573530000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61464-8_51"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614647","9783540685968"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-61464-8_51","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}