{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:29:14Z","timestamp":1725568154667},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405597"},{"type":"electronic","value":"9783540450856"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45085-6_11","type":"book-chapter","created":{"date-parts":[[2010,10,26]],"date-time":"2010-10-26T13:13:30Z","timestamp":1288098810000},"page":"136-150","source":"Crossref","is-referenced-by-count":15,"title":["\u22cc"],"prefix":"10.1007","author":[{"given":"Dimitri","family":"Hendriks","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vincent","family":"van Oostrom","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"11_CR1","doi-asserted-by":"publisher","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. Journal of Functional Programming\u00a01(4), 375\u2013416 (1991)","journal-title":"Journal of Functional Programming"},{"key":"11_CR2","volume-title":"The Optimal Implementation of Functional Programming Languages","author":"A. Asperti","year":"1998","unstructured":"Asperti, A., Guerrini, S.: The Optimal Implementation of Functional Programming Languages. Cambridge University Press, Cambridge (1998)"},{"key":"11_CR3","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"H.P. Barendregt","year":"1984","unstructured":"Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol.\u00a0103. North-Holland, Amsterdam (1984)"},{"key":"11_CR4","unstructured":"Baro, S., Maurel, F.: The q\u03bd and q\u03bdk calculi: name capture and control. PPS pr\u00e9publication 16, Universit\u00e9 Denis Diderot (2003)"},{"key":"11_CR5","unstructured":"Berkling, K.J.: A symmetric complement to the lambda-calculus. Interner Bericht ISF-76-7, GMD, D-5205, St. Augustin 1, West Germany (1976)"},{"issue":"1","key":"11_CR6","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1017\/S0956796899003366","volume":"9","author":"R.S. Bird","year":"1999","unstructured":"Bird, R.S., Paterson, R.A.: De Bruijn notation as a nested datatype. Journal of Functional Programming\u00a09(1), 77\u201391 (1999)","journal-title":"Journal of Functional Programming"},{"key":"11_CR7","unstructured":"Blom, S.C.C.: Term Graph Rewriting, syntax and semantics. PhD thesis, Vrije Universiteit Amsterdam (2001)"},{"key":"11_CR8","unstructured":"Bonelli, E.: Substitutions explicites et r\u00e9\u00e9criture de termes. PhD thesis, Universit\u00e9 Paris XI (2001)"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/BFb0053547","volume-title":"Foundations of Software Science and Computation Structures","author":"L. Cardelli","year":"1998","unstructured":"Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol.\u00a01378, pp. 140\u2013155. Springer, Heidelberg (1998)"},{"key":"11_CR10","unstructured":"Chen, C., Xi, H.: Meta-programming through typeful code representation, \n                    \n                      http:\/\/www.cs.bu.edu\/~hwxi\/"},{"key":"11_CR11","doi-asserted-by":"publisher","first-page":"346","DOI":"10.2307\/1968337","volume":"33","author":"A. Church","year":"1932","unstructured":"Church, A.: A set of postulates for the foundation of logic. Annals of Mathematics\u00a033, 346\u2013366 (1932)","journal-title":"Annals of Mathematics"},{"key":"11_CR12","unstructured":"Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications, \n                    \n                      http:\/\/www.grappa.univ-lille3.fr\/tata"},{"key":"11_CR13","doi-asserted-by":"publisher","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. Mathematical Structures for Computer Science\u00a011, 169\u2013206 (2001)","journal-title":"Mathematical Structures for Computer Science"},{"key":"11_CR14","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":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation. Indagationes Mathematicae\u00a034, 381\u2013392 (1972)","journal-title":"Indagationes Mathematicae"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/3-540-46432-8_5","volume-title":"Foundation of Software Science and Computation Structures","author":"R. Cosmo Di","year":"2000","unstructured":"Di Cosmo, R., Kesner, D., Polonovski, E.: Proof nets and explicit substitutions. In: Tiuryn, J. (ed.) FOSSACS 2000. LNCS, vol.\u00a01784, pp. 63\u201381. Springer, Heidelberg (2000)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BFb0105404","volume-title":"Theorem Proving in Higher Order Logics","author":"A.D. Gordon","year":"1996","unstructured":"Gordon, A.D., Melham, T.F.: Five axioms of alpha-conversion. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 173\u2013190. Springer, Heidelberg (1996)"},{"issue":"5","key":"11_CR17","doi-asserted-by":"publisher","first-page":"725","DOI":"10.1093\/logcom\/6.5.725","volume":"6","author":"M. Hollenberg","year":"1996","unstructured":"Hollenberg, M., Vermeulen, C.F.M.: Counting variables in a dynamic setting. Journal of Logic and Computation\u00a06(5), 725\u2013744 (1996)","journal-title":"Journal of Logic and Computation"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/3-540-56393-8_2","volume-title":"Conditional Term Rewriting Systems","author":"S. Kahrs","year":"1993","unstructured":"Kahrs, S.: Context rewriting. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol.\u00a0656, pp. 21\u201335. Springer, Heidelberg (1993)"},{"key":"11_CR19","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1145\/96709.96718","volume-title":"POPL 1990","author":"Y. Lafont","year":"1990","unstructured":"Lafont, Y.: Interaction nets. In: POPL 1990, pp. 95\u2013108. ACM Press, New York (1990)"},{"key":"11_CR20","series-title":"London Mathematical Society Lecture Note Series","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1017\/CBO9780511629150.012","volume-title":"Advances in Linear Logic","author":"Y. Lafont","year":"1995","unstructured":"Lafont, Y.: From proof-nets to interaction nets. In: Girard, J.-Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic. London Mathematical Society Lecture Note Series, vol.\u00a0222, pp. 225\u2013248. Cambridge University Press, Cambridge (1995)"},{"key":"11_CR21","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1145\/96709.96711","volume-title":"POPL 1990","author":"J. Lamping","year":"1990","unstructured":"Lamping, J.: An algorithm for optimal lambda calculus reduction. In: POPL 1990, pp. 16\u201330. ACM Press, New York (1990)"},{"key":"11_CR22","unstructured":"L\u00e9vy, J.-J.: R\u00e9ductions correctes et optimales dans le \u03bb-calcul. Th\u00e8se de doctorat d\u2019\u00b4etat, Universit\u00e9 Paris VII (1978)"},{"key":"11_CR23","first-page":"176","volume-title":"LICS 1998","author":"J. Parrow","year":"1998","unstructured":"Parrow, J.: The fusion calculus: Expressiveness and symmetry in mobile processes. In: LICS 1998, pp. 176\u2013185. IEEE Computer Society, Los Alamitos (1998)"},{"key":"11_CR24","unstructured":"Schroer, D.E.: The Church\u2013Rosser Theorem. PhD thesis, Cornell University (1965)"},{"key":"11_CR25","unstructured":"Terese. Term Rewriting Systems. Cambridge University Press, Cambridge (2003)"},{"key":"11_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/3-540-45127-7_23","volume-title":"Rewriting Techniques and Applications","author":"R. Vestergaard","year":"2001","unstructured":"Vestergaard, R., Brotherston, J.: A formalised first-order confluence proof for the \u03bb-calculus using one-sorted variable names. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol.\u00a02051, pp. 306\u2013321. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-19"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45085-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,17]],"date-time":"2019-01-17T22:54:25Z","timestamp":1547765665000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45085-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405597","9783540450856"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45085-6_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}