{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,7]],"date-time":"2023-10-07T12:33:23Z","timestamp":1696682003948},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,3,11]],"date-time":"2011-03-11T00:00:00Z","timestamp":1299801600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2012,8]]},"DOI":"10.1007\/s10817-011-9222-5","type":"journal-article","created":{"date-parts":[[2011,3,10]],"date-time":"2011-03-10T13:31:30Z","timestamp":1299763890000},"page":"275-300","source":"Crossref","is-referenced-by-count":2,"title":["On Explicit Substitution with Names"],"prefix":"10.1007","volume":"49","author":[{"given":"Kristoffer H.","family":"Rose","sequence":"first","affiliation":[]},{"given":"Roel","family":"Bloo","sequence":"additional","affiliation":[]},{"given":"Fr\u00e9d\u00e9ric","family":"Lang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,3,11]]},"reference":[{"issue":"4","key":"9222_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., L\u00e9vy, J.J.: Explicit substitutions. J. Funct. Program. 1(4), 375\u2013416 (1991)","journal-title":"J. Funct. Program."},{"key":"9222_CR2","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1999)","DOI":"10.1017\/CBO9781139172752"},{"key":"9222_CR3","unstructured":"Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics, revised edn. North-Holland (1984)"},{"key":"9222_CR4","unstructured":"Benaissa, Z.E.A., Briaud, D., Lescanne, P., Rouyer-Degli, J.: \u03bb\u03c5, a calculus of explicit substitutions which preserves strong normalisation. Rapport de Recherche 2477, INRIA, Lorraine, Techn\u00f4pole de Nancy-Brabois, Campus Scientifique, 615 rue de Jardin Botanique, BP 101, F-54600 Villers l\u00e8s Nancy. http:\/\/www.loria.fr\/\u00a0lescanne\/PUBLICATIONS\/RR-2477.PS (1995)"},{"key":"9222_CR5","unstructured":"Bezem, M., Klop, J.W., de Vrijer, R.: Term Rewriting Systems. Cambridge University Press, known as the \u201cTeReSe\u201d book (2003)"},{"key":"9222_CR6","unstructured":"Bloo, R.: Preservation of Termination for Explicit Substitution. PhD thesis, Technische Universiteit Eindhoven, iPA Dissertation Series 1997-05 (1997)"},{"issue":"1\u20132","key":"9222_CR7","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1016\/S0304-3975(97)00183-7","volume":"211","author":"R Bloo","year":"1999","unstructured":"Bloo, R., Geuvers, H.: Explicit substitution: on the edge of strong normalisation. Theor. Comp. Sci. 211(1\u20132), 375\u2013395 (1999)","journal-title":"Theor. Comp. Sci."},{"key":"9222_CR8","unstructured":"Bloo, R., Rose, K.H.: Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection. In: CSN \u201995\u2014Computing Science in the Netherlands, Koninklijke Jaarbeurs, pp. 62\u201372. Utrecht (1995)"},{"key":"9222_CR9","first-page":"62","volume-title":"RTA 2000\u201411th International Conference on Rewriting Techniques and Applications","author":"E Bonelli","year":"2000","unstructured":"Bonelli, E., Kesner, D., R\u00edos, A.: A de Bruijn notation for higher-order rewriting. In: RTA 2000\u201411th International Conference on Rewriting Techniques and Applications. Lecture Notes in Computer Science, pp. 62\u201379, no. 1833. Springer-Verlag, Norwick (2000)"},{"key":"9222_CR10","doi-asserted-by":"crossref","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation with application to the Church\u2013Rosser theorem. Koninklijke Nederlandse Akademie van Wetenschappen, Series A, Mathematical Sciences 75:381\u2013392, also chapter C.2 of (Nederpelt et al. 1994) (1972)","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"9222_CR11","volume-title":"The Calculi of Lambda-Conversion","author":"A Church","year":"1941","unstructured":"Church A.: The Calculi of Lambda-Conversion. Princeton University Press, Princeton, NJ (1941)"},{"key":"9222_CR12","doi-asserted-by":"crossref","first-page":"472","DOI":"10.1090\/S0002-9947-1936-1501858-0","volume":"39","author":"A Church","year":"1935","unstructured":"Church, A., Rosser, J.B.: Some properties of conversion. Trans. AMS 39, 472\u2013482 (1935)","journal-title":"Trans. AMS"},{"key":"9222_CR13","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1016\/0304-3975(91)90230-Y","volume":"82","author":"PL Curien","year":"1991","unstructured":"Curien, P.L.: An abstract framework for environment machines. Theor. Comp. Sci. 82, 389\u2013402 (1991)","journal-title":"Theor. Comp. Sci."},{"issue":"2","key":"9222_CR14","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1145\/226643.226675","volume":"43","author":"PL Curien","year":"1996","unstructured":"Curien, P.L., Hardin, T., L\u00e9vy, J.J.: Confluence properties of weak and strong calculi of explicit substitutions. J. ACM 43(2), 362\u2013397 (1996)","journal-title":"J. ACM"},{"key":"9222_CR15","unstructured":"Curry, H.B., Feys, R.: Combinatory Logic, vol. I. North-Holland (1958)"},{"issue":"1","key":"9222_CR16","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1017\/S0960129500003224","volume":"11","author":"R David","year":"2001","unstructured":"David, R., Guillaume, B.: A \u03bb-calculus with explicit weakening and explicit substitution. Math. Struct. Comput. Sci. 11(1), 169\u2013206 (2001)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9222_CR17","unstructured":"Dershowitz, N.: Termination of rewriting. J. Symb. Comput. 3(1), 69\u2013116. Corrigendum: 4(3), 409\u2013410 (1987)"},{"key":"9222_CR18","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B., chap. 6, pp. 244\u2013320. Elsevier (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"issue":"3","key":"9222_CR19","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1017\/S0960129502003791","volume":"13","author":"R Cosmo Di","year":"2003","unstructured":"Di Cosmo, R., Kesner, D., Polonovski, E.: Proof nets and explicit substitutions. Math. Struct. Comput. Sci. 13(3), 409\u2013450 (2003)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"6","key":"9222_CR20","doi-asserted-by":"crossref","first-page":"917","DOI":"10.1016\/j.ic.2006.12.002","volume":"205","author":"M Fern\u00e1ndez","year":"2007","unstructured":"Fern\u00e1ndez, M., Gabbay, M.J.: Nominal rewriting. Inf. Comput. 205(6), 917\u2013965 (2007). doi: 10.1016\/j.ic.2006.12.002","journal-title":"Inf. Comput."},{"key":"9222_CR21","first-page":"220","volume-title":"CSL \u201999\u201413th International Workshop on Computer Science Logic. Lecture Notes in Computer Science, vol. 1683","author":"M Fern\u00e1ndez","year":"1999","unstructured":"Fern\u00e1ndez, M., Mackie, I.: Closed reductions in the lambda-calculus. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL \u201999\u201413th International Workshop on Computer Science Logic. Lecture Notes in Computer Science, vol. 1683, pp. 220\u2013234. Springer-Verlag, Madrid (1999)","edition":"1683"},{"issue":"6","key":"9222_CR22","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1007\/s00200-005-0169-9","volume":"15","author":"M Fern\u00e1ndez","year":"2005","unstructured":"Fern\u00e1ndez, M., Mackie, I., Sinot, F.R.: Lambda-calculus with director strings. Appl. Algebra Eng. Commun. Comput. 15(6), 393\u2013437 (2005)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"9222_CR23","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(89)90105-9","volume":"65","author":"T Hardin","year":"1989","unstructured":"Hardin, T.: Confluence results for the pure strong categorical logic CCL; \u03bb-calculi as subsystems of CCL. Theor. Comp. Sci. 65, 291\u2013342 (1989)","journal-title":"Theor. Comp. Sci."},{"issue":"3","key":"9222_CR24","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1142\/S0129054193000146","volume":"4","author":"F Kamareddine","year":"1993","unstructured":"Kamareddine, F., Nederpelt, R.P.: On stepwise explicit substitution. Int. J. Found. Comput. Sci. 4(3), 197\u2013240 (1993)","journal-title":"Int. J. Found. Comput. Sci."},{"issue":"1\u20132","key":"9222_CR25","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/S0304-3975(98)00166-2","volume":"238","author":"D Kesner","year":"2000","unstructured":"Kesner, D.: Confluence properties of extensional and non-extensional \u03bb-calculi with explicit substitution. Theor. Comp. Sci. 238(1\u20132), 183\u2013220 (2000)","journal-title":"Theor. Comp. Sci."},{"key":"9222_CR26","first-page":"238","volume-title":"CSL 2007\u2014Computer Science and Logic. Lecture Notes in Computer Science, vol. 4646","author":"D Kesner","year":"2007","unstructured":"Kesner, D.: The theory of explicit substitutions revisited. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007\u2014Computer Science and Logic. Lecture Notes in Computer Science, vol. 4646, pp. 238\u2013252. Springer-Verlag, Lausanne (2007)","edition":"4646"},{"issue":"3:1","key":"9222_CR27","first-page":"1","volume":"5","author":"D Kesner","year":"2009","unstructured":"Kesner, D.: A theory of explicit substitutions with safe and full composition. Logical Methods in Computer Science 5(3:1), 1\u201329 (2009). http:\/\/www.lmcs-online.org\/ojs\/viewarticle.php?id=480","journal-title":"Logical Methods in Computer Science"},{"key":"9222_CR28","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1016\/j.ic.2006.08.008","volume":"205","author":"D Kesner","year":"2007","unstructured":"Kesner, D., Lengrand, S.: Resource operators for the \u03bb-calculus. Inf. Comput. 205, 419\u2013473 (2007)","journal-title":"Inf. Comput."},{"key":"9222_CR29","unstructured":"Klop, J.W.: Term rewriting systems. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 2, chap. 1, pp. 1\u2013116. Oxford University Press (1992)"},{"key":"9222_CR30","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","volume":"121","author":"JW Klop","year":"1993","unstructured":"Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. Theor. Comp. Sci. 121, 279\u2013308 (1993)","journal-title":"Theor. Comp. Sci."},{"key":"9222_CR31","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1093\/comjnl\/6.4.308","volume":"6","author":"PJ Landin","year":"1964","unstructured":"Landin, P.J.: The mechanical evaluation of expressions. Comput. J. 6, 308\u2013320 (1964)","journal-title":"Comput. J."},{"key":"9222_CR32","unstructured":"Lang, F., Rose, K.H.: Two equivalent calculi of explicit substitution with confluence on meta-terms and preservation of strong normalization (one with names and one first order). Presented at WESTAPP \u201998\u2014The First International Workshop on Explicit Substitutions: Theory and Applications to Programs and Proofs (Tsukuba, Japan) (1998). http:\/\/www.inrialpes.fr\/vasy\/people\/Frederic.Lang\/westapp98.ps.gz"},{"key":"9222_CR33","doi-asserted-by":"crossref","unstructured":"Lescanne, P.: From \u03bb\u03c3 to \u03bb\u03c5: a journey through calculi of explicit substitutions. In: POPL \u201994\u201421st Annual ACM Symposium on Principles of Programming Languages, pp. 60\u201369. Portland, Oregon (1994)","DOI":"10.1145\/174675.174707"},{"key":"9222_CR34","doi-asserted-by":"crossref","unstructured":"Lins, R.D.: A new formula for the execution of catgorical combinators. In: CADE \u201986\u2014Conference on Automated Deduction. Lecture Notes in Computer Science, vol. 230, pp. 89\u201398. Springer-Verlag (1986)","DOI":"10.1007\/3-540-16780-3_82"},{"issue":"7","key":"9222_CR35","first-page":"769","volume":"10","author":"RD Lins","year":"2004","unstructured":"Lins, R.D.: Partial categorical multi-combinators and Church\u2013Rosser theorems. J. Univers. Comput. Sci. 10(7), 769\u2013788 (2004)","journal-title":"J. Univers. Comput. Sci."},{"key":"9222_CR36","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/BFb0014062","volume-title":"TLCA \u201995\u2014Int. Conf. on Typed Lambda Calculus and Applications. Lecture Notes in Computer Science","author":"PA Melli\u00e8s","year":"1995","unstructured":"Melli\u00e8s, P.A.: Typed \u03bb-calculi with explicit substitution may not terminate. In: Dezani-Ciancaglini, M., Plotkin, G.D. (eds.) TLCA \u201995\u2014Int. Conf. on Typed Lambda Calculus and Applications. Lecture Notes in Computer Science, pp. 328\u2013334, no. 902. Springer-Verlag, Edinburgh (1995)"},{"key":"9222_CR37","unstructured":"Mitschke, G.: Eine algebraische Behandlung von \u03bb-K-Kalk\u00fcl und Kombinatorischer Logik. PhD thesis, Rheinischen Friedrich-Wilhelms U., Bonn, Germany (1970)"},{"key":"9222_CR38","unstructured":"van Raamsdonk, F.: Confluence and Normalization for Higher-order Rewriting. PhD thesis, Amsterdam University (1996)"},{"issue":"2","key":"9222_CR39","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1137\/0214028","volume":"14","author":"G Revesz","year":"1985","unstructured":"Revesz, G.: Axioms for the theory of lambda-conversion. SIAM J. Comput. 14(2), 373\u2013382 (1985)","journal-title":"SIAM J. Comput."},{"key":"9222_CR40","doi-asserted-by":"crossref","unstructured":"Ritter, E.: Characterising explicit substitutions which preserve termination. In: Girard, J.Y. (ed.) TLCA \u201999\u2014Int. Conf. on Typed Lambda Calculus and Applications. Lecture Notes in Computer Science, pp. 325\u2013339, no. 1581. Springer-Verlag, L\u2019Aquila (1999)","DOI":"10.1007\/3-540-48959-2_23"},{"key":"9222_CR41","first-page":"248","volume-title":"ICALP \u201997\u201424th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 1256","author":"E Ritter","year":"1997","unstructured":"Ritter, E., de Paiva, V.: On explicit substitution and names (extended abstract). In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP \u201997\u201424th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 1256, pp. 248\u2013258. Springer-Verlag, Bologna (1997)","edition":"1256"},{"key":"9222_CR42","unstructured":"Rose, K.H.: Explicit cyclic substitutions. In: Rusinowitch, M., R\u00e9my, J.L. (eds.) CTRS \u201992\u20143rd International Workshop on Conditional Term Rewriting Systems. Lecture Notes in Computer Science, pp. 36\u201350, no. 656. Springer-Verlag, Pont-a-Mousson (1992)"},{"key":"9222_CR43","unstructured":"Rose, K.H.: Explicit substitution \u2013 tutorial & survey. Lecture Series LS\u201396\u20133, BRICS, Dept. of Computer Science, University of Aarhus, Denmark (1996). ftp:\/\/ftp.brics.dk\/LS\/96\/3\/BRICS-LS-96-3.ps.gz"},{"key":"9222_CR44","unstructured":"Rose, K.H.: Operational reduction models for functional programming languages. PhD thesis, DIKU, Univ. of Copenhagen (1996). http:\/\/www.diku.dk\/OLD\/publikationer\/tekniske.rapporter\/rapporter\/96-01.pdf , DIKU report 96\/1"},{"key":"9222_CR45","unstructured":"Rose, K.H., Bloo, R., Lang, F.: On explicit substitution with names. IBM Research Report RC24909, IBM Thomas J. Watson Research Center, P.O. Box 704, Yorktown Heights, NY 10598, USA (2009). http:\/\/domino.research.ibm.com\/library\/cyberdig.nsf\/reportnumber\/rc24909"},{"issue":"1","key":"9222_CR46","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1145\/321738.321750","volume":"20","author":"BK Rosen","year":"1973","unstructured":"Rosen, B.K.: Tree-manipulating systems and Church\u2013Rosser theorems. J. ACM 20(1), 160\u2013187 (1973)","journal-title":"J. ACM"},{"key":"9222_CR47","first-page":"169","volume-title":"RTA 2007\u201418th International Conference on Term Rewriting and Applications. Lecture Notes in Computer Science, vol. 4533","author":"JE Santo","year":"2007","unstructured":"Santo, J.E.: Delayed substitutions. In: Baader, F. (ed.) RTA 2007\u201418th International Conference on Term Rewriting and Applications. Lecture Notes in Computer Science, vol. 4533, pp. 169\u2013183. Springer-Verlag, Paris (2007)","edition":"4533"},{"key":"9222_CR48","unstructured":"Urbanm, C.: How to prove false using the variable convention. Poster at the occasion of Prof. Mike D. Gordon\u2019s 60th birthday (2008). Available from http:\/\/www4.in.tum.de\/~urbanc\/Publications\/mike-poster-08.pdf"},{"issue":"4","key":"9222_CR49","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1007\/s10817-008-9097-2","volume":"40","author":"C Urban","year":"2008","unstructured":"Urban, C.: Nominal techniques in Isabelle\/HOL. J Autom Reasoning 40(4), 327\u2013356 (2008)","journal-title":"J Autom Reasoning"},{"issue":"1","key":"9222_CR50","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1137\/0219005","volume":"19","author":"H Yokouchi","year":"1990","unstructured":"Yokouchi, H., Hikita, T.: A rewriting system for categorical combinators with multiple arguments. SIAM J. Comput. 19(1), 78\u201397 (1990)","journal-title":"SIAM J. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-011-9222-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-011-9222-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-011-9222-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,17]],"date-time":"2020-06-17T07:27:00Z","timestamp":1592378820000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-011-9222-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,3,11]]},"references-count":50,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["9222"],"URL":"https:\/\/doi.org\/10.1007\/s10817-011-9222-5","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,3,11]]}}}